Theorem xabfin ≪ | index | src | ≫

theorem xabfin (A: set) (G: wff) {x: nat} (B: set x):
  $ G -> finite A $ >
  $ G /\ x e. A -> finite B $ >
  $ G -> finite (X\ x e. A, B) $;

Step	Hyp	Ref	Expression
1		finss	X\ x e. A, B C_ Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) -> finite (Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A))) -> finite (X\ x e. A, B)
2		cbvxabs	X\ x e. A, B == X\ a1 e. A, (S[a1 / x] B)
3		eqlower	finite (S[a1 / x] B) <-> S[a1 / x] B == lower (S[a1 / x] B)
4		nfv	F/ x G /\ a1 e. A
5		nfsbs1	FS/ x S[a1 / x] B
6	5	nffin	F/ x finite (S[a1 / x] B)
7	4, 6	nfim	F/ x G /\ a1 e. A -> finite (S[a1 / x] B)
8		hyp h2	G /\ x e. A -> finite B
9		eleq1	x = a1 -> (x e. A <-> a1 e. A)
10	9	aneq2d	x = a1 -> (G /\ x e. A <-> G /\ a1 e. A)
11		sbsq	x = a1 -> B == S[a1 / x] B
12	11	fineqd	x = a1 -> (finite B <-> finite (S[a1 / x] B))
13	10, 12	imeqd	x = a1 -> (G /\ x e. A -> finite B <-> G /\ a1 e. A -> finite (S[a1 / x] B))
14	7, 8, 13	sbethh	G /\ a1 e. A -> finite (S[a1 / x] B)
15	3, 14	sylib	G /\ a1 e. A -> S[a1 / x] B == lower (S[a1 / x] B)
16	15	xabeq2da	G -> X\ a1 e. A, (S[a1 / x] B) == X\ a1 e. A, lower (S[a1 / x] B)
17	2, 16	syl5eqs	G -> X\ x e. A, B == X\ a1 e. A, lower (S[a1 / x] B)
18		eqscom	X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A) == Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) -> Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) == X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
19		xabconst	X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A) == Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A))
20	18, 19	ax_mp	Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) == X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
21	20	a1i	G -> Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) == X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
22	17, 21	sseqd	G -> (X\ x e. A, B C_ Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) <-> X\ a1 e. A, lower (S[a1 / x] B) C_ X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A) )
23		elssuni	lower (S[a1 / x] B) e. (\ a2, lower (S[a2 / x] B)) '' A -> lower (S[a1 / x] B) C_ sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
24		elimai	a1, lower (S[a1 / x] B) e. \ a2, lower (S[a2 / x] B) -> a1 e. A -> lower (S[a1 / x] B) e. (\ a2, lower (S[a2 / x] B)) '' A
25		ellam	a1, lower (S[a1 / x] B) e. \ a2, lower (S[a2 / x] B) <-> E. a2 a1, lower (S[a1 / x] B) = a2, lower (S[a2 / x] B)
26		id	a2 = a1 -> a2 = a1
27	26	sbseq1d	a2 = a1 -> S[a2 / x] B == S[a1 / x] B
28	27	lowereqd	a2 = a1 -> lower (S[a2 / x] B) = lower (S[a1 / x] B)
29	26, 28	preqd	a2 = a1 -> a2, lower (S[a2 / x] B) = a1, lower (S[a1 / x] B)
30	29	eqeq2d	a2 = a1 -> (a1, lower (S[a1 / x] B) = a2, lower (S[a2 / x] B) <-> a1, lower (S[a1 / x] B) = a1, lower (S[a1 / x] B))
31	30	iexe	a1, lower (S[a1 / x] B) = a1, lower (S[a1 / x] B) -> E. a2 a1, lower (S[a1 / x] B) = a2, lower (S[a2 / x] B)
32		eqid	a1, lower (S[a1 / x] B) = a1, lower (S[a1 / x] B)
33	31, 32	ax_mp	E. a2 a1, lower (S[a1 / x] B) = a2, lower (S[a2 / x] B)
34	25, 33	mpbir	a1, lower (S[a1 / x] B) e. \ a2, lower (S[a2 / x] B)
35	24, 34	ax_mp	a1 e. A -> lower (S[a1 / x] B) e. (\ a2, lower (S[a2 / x] B)) '' A
36	35	anwr	G /\ a1 e. A -> lower (S[a1 / x] B) e. (\ a2, lower (S[a2 / x] B)) '' A
37	23, 36	syl	G /\ a1 e. A -> lower (S[a1 / x] B) C_ sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
38	37	xabssd	G -> X\ a1 e. A, lower (S[a1 / x] B) C_ X\ a1 e. A, sUnion ((\ a2, lower (S[a2 / x] B)) '' A)
39	22, 38	mpbird	G -> X\ x e. A, B C_ Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A))
40		xpfin	finite A -> finite (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)) -> finite (Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)))
41		hyp h	G -> finite A
42		finuni	finite ((\ a2, lower (S[a2 / x] B)) '' A) -> finite (sUnion ((\ a2, lower (S[a2 / x] B)) '' A))
43		finlamima	finite A -> finite ((\ a2, lower (S[a2 / x] B)) '' A)
44	43, 41	syl	G -> finite ((\ a2, lower (S[a2 / x] B)) '' A)
45	42, 44	syl	G -> finite (sUnion ((\ a2, lower (S[a2 / x] B)) '' A))
46	40, 41, 45	sylc	G -> finite (Xp A (sUnion ((\ a2, lower (S[a2 / x] B)) '' A)))
47	1, 39, 46	sylc	G -> finite (X\ x e. A, B)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)