Theorem tfinnn 4534

Description: T-raising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
tfinnn	|- ((N e. Nn /\ A C_ Nn /\ A e. N) -> {a | E.x e. A a = Tfin x} e. Tfin N)

Distinct variable groups:   N,a,x   A,a,x

Proof of Theorem tfinnn

Dummy variables y n b k w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfinnnlem1 4533	. . . . 5 |- {n | A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n)} e. _V
2		tfineq 4488	. . . . . . . . . 10 |- (n = 0c -> Tfin n = Tfin 0c)
3		tfin0c 4497	. . . . . . . . . 10 |- Tfin 0c = 0c
4	2, 3	syl6eq 2401	. . . . . . . . 9 |- (n = 0c -> Tfin n = 0c)
5	4	eleq2d 2420	. . . . . . . 8 |- (n = 0c -> ({a | E.x e. y a = Tfin x} e. Tfin n <-> {a | E.x e. y a = Tfin x} e. 0c))
6	5	imbi2d 307	. . . . . . 7 |- (n = 0c -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c)))
7	6	raleqbi1dv 2815	. . . . . 6 |- (n = 0c -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> A.y e. 0c (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c)))
8		df-ral 2619	. . . . . . 7 |- (A.y e. 0c (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c) <-> A.y(y e. 0c -> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c)))
9		el0c 4421	. . . . . . . . 9 |- (y e. 0c <-> y = (/))
10		el0c 4421	. . . . . . . . . . 11 |- ({a | E.x e. y a = Tfin x} e. 0c <-> {a | E.x e. y a = Tfin x} = (/))
11		ab0 3569	. . . . . . . . . . 11 |- ({a | E.x e. y a = Tfin x} = (/) <-> A.a -. E.x e. y a = Tfin x)
12	10, 11	bitri 240	. . . . . . . . . 10 |- ({a | E.x e. y a = Tfin x} e. 0c <-> A.a -. E.x e. y a = Tfin x)
13	12	imbi2i 303	. . . . . . . . 9 |- ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c) <-> (y C_ Nn -> A.a -. E.x e. y a = Tfin x))
14	9, 13	imbi12i 316	. . . . . . . 8 |- ((y e. 0c -> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c)) <-> (y = (/) -> (y C_ Nn -> A.a -. E.x e. y a = Tfin x)))
15	14	albii 1566	. . . . . . 7 |- (A.y(y e. 0c -> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c)) <-> A.y(y = (/) -> (y C_ Nn -> A.a -. E.x e. y a = Tfin x)))
16		0ex 4110	. . . . . . . 8 |- (/) e. _V
17		sseq1 3292	. . . . . . . . 9 |- (y = (/) -> (y C_ Nn <-> (/) C_ Nn ))
18		rexeq 2808	. . . . . . . . . . 11 |- (y = (/) -> (E.x e. y a = Tfin x <-> E.x e. (/) a = Tfin x))
19	18	notbid 285	. . . . . . . . . 10 |- (y = (/) -> (-. E.x e. y a = Tfin x <-> -. E.x e. (/) a = Tfin x))
20	19	albidv 1625	. . . . . . . . 9 |- (y = (/) -> (A.a -. E.x e. y a = Tfin x <-> A.a -. E.x e. (/) a = Tfin x))
21	17, 20	imbi12d 311	. . . . . . . 8 |- (y = (/) -> ((y C_ Nn -> A.a -. E.x e. y a = Tfin x) <-> ((/) C_ Nn -> A.a -. E.x e. (/) a = Tfin x)))
22	16, 21	ceqsalv 2885	. . . . . . 7 |- (A.y(y = (/) -> (y C_ Nn -> A.a -. E.x e. y a = Tfin x)) <-> ((/) C_ Nn -> A.a -. E.x e. (/) a = Tfin x))
23	8, 15, 22	3bitri 262	. . . . . 6 |- (A.y e. 0c (y C_ Nn -> {a | E.x e. y a = Tfin x} e. 0c) <-> ((/) C_ Nn -> A.a -. E.x e. (/) a = Tfin x))
24	7, 23	syl6bb 252	. . . . 5 |- (n = 0c -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> ((/) C_ Nn -> A.a -. E.x e. (/) a = Tfin x)))
25		tfineq 4488	. . . . . . . 8 |- (n = k -> Tfin n = Tfin k)
26	25	eleq2d 2420	. . . . . . 7 |- (n = k -> ({a | E.x e. y a = Tfin x} e. Tfin n <-> {a | E.x e. y a = Tfin x} e. Tfin k))
27	26	imbi2d 307	. . . . . 6 |- (n = k -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)))
28	27	raleqbi1dv 2815	. . . . 5 |- (n = k -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)))
29		tfineq 4488	. . . . . . . . 9 |- (n = (k +o 1c) -> Tfin n = Tfin (k +o 1c))
30	29	eleq2d 2420	. . . . . . . 8 |- (n = (k +o 1c) -> ({a | E.x e. y a = Tfin x} e. Tfin n <-> {a | E.x e. y a = Tfin x} e. Tfin (k +o 1c)))
31	30	imbi2d 307	. . . . . . 7 |- (n = (k +o 1c) -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin (k +o 1c))))
32	31	raleqbi1dv 2815	. . . . . 6 |- (n = (k +o 1c) -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> A.y e. (k +o 1c)(y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin (k +o 1c))))
33		sseq1 3292	. . . . . . . 8 |- (y = z -> (y C_ Nn <-> z C_ Nn ))
34		rexeq 2808	. . . . . . . . . 10 |- (y = z -> (E.x e. y a = Tfin x <-> E.x e. z a = Tfin x))
35	34	abbidv 2467	. . . . . . . . 9 |- (y = z -> {a | E.x e. y a = Tfin x} = {a | E.x e. z a = Tfin x})
36	35	eleq1d 2419	. . . . . . . 8 |- (y = z -> ({a | E.x e. y a = Tfin x} e. Tfin (k +o 1c) <-> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c)))
37	33, 36	imbi12d 311	. . . . . . 7 |- (y = z -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin (k +o 1c)) <-> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c))))
38	37	cbvralv 2835	. . . . . 6 |- (A.y e. (k +o 1c)(y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin (k +o 1c)) <-> A.z e. (k +o 1c)(z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c)))
39	32, 38	syl6bb 252	. . . . 5 |- (n = (k +o 1c) -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> A.z e. (k +o 1c)(z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c))))
40		tfineq 4488	. . . . . . . 8 |- (n = N -> Tfin n = Tfin N)
41	40	eleq2d 2420	. . . . . . 7 |- (n = N -> ({a | E.x e. y a = Tfin x} e. Tfin n <-> {a | E.x e. y a = Tfin x} e. Tfin N))
42	41	imbi2d 307	. . . . . 6 |- (n = N -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin N)))
43	42	raleqbi1dv 2815	. . . . 5 |- (n = N -> (A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n) <-> A.y e. N (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin N)))
44		rex0 3563	. . . . . . 7 |- -. E.x e. (/) a = Tfin x
45	44	ax-gen 1546	. . . . . 6 |- A.a -. E.x e. (/) a = Tfin x
46	45	a1i 10	. . . . 5 |- ((/) C_ Nn -> A.a -. E.x e. (/) a = Tfin x)
47		elsuc 4413	. . . . . . . . . . 11 |- (z e. (k +o 1c) <-> E.b e. k E.w e. ∼ bz = (b u. {w}))
48		sseq1 3292	. . . . . . . . . . . . . . . . . 18 |- (y = b -> (y C_ Nn <-> b C_ Nn ))
49		rexeq 2808	. . . . . . . . . . . . . . . . . . . 20 |- (y = b -> (E.x e. y a = Tfin x <-> E.x e. b a = Tfin x))
50	49	abbidv 2467	. . . . . . . . . . . . . . . . . . 19 |- (y = b -> {a | E.x e. y a = Tfin x} = {a | E.x e. b a = Tfin x})
51	50	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 |- (y = b -> ({a | E.x e. y a = Tfin x} e. Tfin k <-> {a | E.x e. b a = Tfin x} e. Tfin k))
52	48, 51	imbi12d 311	. . . . . . . . . . . . . . . . 17 |- (y = b -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k) <-> (b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k)))
53	52	rspcv 2951	. . . . . . . . . . . . . . . 16 |- (b e. k -> (A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k) -> (b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k)))
54	53	ad2antrl 708	. . . . . . . . . . . . . . 15 |- ((k e. Nn /\ (b e. k /\ w e. ∼ b)) -> (A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k) -> (b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k)))
55		simprl 732	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> b C_ Nn )
56		simp3 957	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn ) /\ {a | E.x e. b a = Tfin x} e. Tfin k) -> {a | E.x e. b a = Tfin x} e. Tfin k)
57		simplrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> w e. ∼ b)
58		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- w e. _V
59	58	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. ∼ b <-> -. w e. b)
60	57, 59	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> -. w e. b)
61		elequ1 1713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = x -> (w e. b <-> x e. b))
62	61	notbid 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = x -> (-. w e. b <-> -. x e. b))
63	60, 62	syl5ibcom 211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> (w = x -> -. x e. b))
64	63	con2d 107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> (x e. b -> -. w = x))
65	64	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) -> -. w = x)
66		simpll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> ((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )))
67		simprr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> w e. Nn )
68	66, 67	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> w e. Nn )
69	66, 55	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> b C_ Nn )
70		simplr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> x e. b)
71	69, 70	sseldd 3274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> x e. Nn )
72		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> Tfin w = Tfin x)
73		tfin11 4493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. Nn /\ x e. Nn /\ Tfin w = Tfin x) -> w = x)
74	68, 71, 72, 73	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) /\ Tfin w = Tfin x) -> w = x)
75	65, 74	mtand 640	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) /\ x e. b) -> -. Tfin w = Tfin x)
76	75	nrexdv 2717	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> -. E.x e. b Tfin w = Tfin x)
77	76	3adant3 975	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn ) /\ {a | E.x e. b a = Tfin x} e. Tfin k) -> -. E.x e. b Tfin w = Tfin x)
78		tfinex 4485	. . . . . . . . . . . . . . . . . . . . . . 23 |- Tfin w e. _V
79		eqeq1 2359	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a = Tfin w -> (a = Tfin x <-> Tfin w = Tfin x))
80	79	rexbidv 2635	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = Tfin w -> (E.x e. b a = Tfin x <-> E.x e. b Tfin w = Tfin x))
81	78, 80	elab 2985	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Tfin w e. {a | E.x e. b a = Tfin x} <-> E.x e. b Tfin w = Tfin x)
82	77, 81	sylnibr 296	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn ) /\ {a | E.x e. b a = Tfin x} e. Tfin k) -> -. Tfin w e. {a | E.x e. b a = Tfin x})
83	78	elsuci 4414	. . . . . . . . . . . . . . . . . . . . 21 |- (({a | E.x e. b a = Tfin x} e. Tfin k /\ -. Tfin w e. {a | E.x e. b a = Tfin x}) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c))
84	56, 82, 83	syl2anc 642	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn ) /\ {a | E.x e. b a = Tfin x} e. Tfin k) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c))
85	84	3expia 1153	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> ({a | E.x e. b a = Tfin x} e. Tfin k -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c)))
86	55, 85	embantd 50	. . . . . . . . . . . . . . . . . 18 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ (b C_ Nn /\ w e. Nn )) -> ((b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c)))
87	86	ex 423	. . . . . . . . . . . . . . . . 17 |- ((k e. Nn /\ (b e. k /\ w e. ∼ b)) -> ((b C_ Nn /\ w e. Nn ) -> ((b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c))))
88	87	com23 72	. . . . . . . . . . . . . . . 16 |- ((k e. Nn /\ (b e. k /\ w e. ∼ b)) -> ((b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k) -> ((b C_ Nn /\ w e. Nn ) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c))))
89		sseq1 3292	. . . . . . . . . . . . . . . . . . 19 |- (z = (b u. {w}) -> (z C_ Nn <-> (b u. {w}) C_ Nn ))
90	58	snss 3838	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. Nn <-> {w} C_ Nn )
91	90	anbi2i 675	. . . . . . . . . . . . . . . . . . . 20 |- ((b C_ Nn /\ w e. Nn ) <-> (b C_ Nn /\ {w} C_ Nn ))
92		unss 3437	. . . . . . . . . . . . . . . . . . . 20 |- ((b C_ Nn /\ {w} C_ Nn ) <-> (b u. {w}) C_ Nn )
93	91, 92	bitr2i 241	. . . . . . . . . . . . . . . . . . 19 |- ((b u. {w}) C_ Nn <-> (b C_ Nn /\ w e. Nn ))
94	89, 93	syl6bb 252	. . . . . . . . . . . . . . . . . 18 |- (z = (b u. {w}) -> (z C_ Nn <-> (b C_ Nn /\ w e. Nn )))
95		rexeq 2808	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (b u. {w}) -> (E.x e. z a = Tfin x <-> E.x e. (b u. {w})a = Tfin x))
96		rexun 3443	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.x e. (b u. {w})a = Tfin x <-> (E.x e. b a = Tfin x \/ E.x e. {w}a = Tfin x))
97	95, 96	syl6bb 252	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (b u. {w}) -> (E.x e. z a = Tfin x <-> (E.x e. b a = Tfin x \/ E.x e. {w}a = Tfin x)))
98	97	abbidv 2467	. . . . . . . . . . . . . . . . . . . 20 |- (z = (b u. {w}) -> {a | E.x e. z a = Tfin x} = {a | (E.x e. b a = Tfin x \/ E.x e. {w}a = Tfin x)})
99		df-sn 3741	. . . . . . . . . . . . . . . . . . . . . . 23 |- { Tfin w} = {a | a = Tfin w}
100		tfineq 4488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = w -> Tfin x = Tfin w)
101	100	eqeq2d 2364	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = w -> (a = Tfin x <-> a = Tfin w))
102	58, 101	rexsn 3768	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.x e. {w}a = Tfin x <-> a = Tfin w)
103	102	abbii 2465	. . . . . . . . . . . . . . . . . . . . . . 23 |- {a | E.x e. {w}a = Tfin x} = {a | a = Tfin w}
104	99, 103	eqtr4i 2376	. . . . . . . . . . . . . . . . . . . . . 22 |- { Tfin w} = {a | E.x e. {w}a = Tfin x}
105	104	uneq2i 3415	. . . . . . . . . . . . . . . . . . . . 21 |- ({a | E.x e. b a = Tfin x} u. { Tfin w}) = ({a | E.x e. b a = Tfin x} u. {a | E.x e. {w}a = Tfin x})
106		unab 3521	. . . . . . . . . . . . . . . . . . . . 21 |- ({a | E.x e. b a = Tfin x} u. {a | E.x e. {w}a = Tfin x}) = {a | (E.x e. b a = Tfin x \/ E.x e. {w}a = Tfin x)}
107	105, 106	eqtr2i 2374	. . . . . . . . . . . . . . . . . . . 20 |- {a | (E.x e. b a = Tfin x \/ E.x e. {w}a = Tfin x)} = ({a | E.x e. b a = Tfin x} u. { Tfin w})
108	98, 107	syl6eq 2401	. . . . . . . . . . . . . . . . . . 19 |- (z = (b u. {w}) -> {a | E.x e. z a = Tfin x} = ({a | E.x e. b a = Tfin x} u. { Tfin w}))
109	108	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 |- (z = (b u. {w}) -> ({a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c) <-> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c)))
110	94, 109	imbi12d 311	. . . . . . . . . . . . . . . . 17 |- (z = (b u. {w}) -> ((z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c)) <-> ((b C_ Nn /\ w e. Nn ) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c))))
111	110	biimprcd 216	. . . . . . . . . . . . . . . 16 |- (((b C_ Nn /\ w e. Nn ) -> ({a | E.x e. b a = Tfin x} u. { Tfin w}) e. ( Tfin k +o 1c)) -> (z = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))))
112	88, 111	syl6 29	. . . . . . . . . . . . . . 15 |- ((k e. Nn /\ (b e. k /\ w e. ∼ b)) -> ((b C_ Nn -> {a | E.x e. b a = Tfin x} e. Tfin k) -> (z = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c)))))
113	54, 112	syld 40	. . . . . . . . . . . . . 14 |- ((k e. Nn /\ (b e. k /\ w e. ∼ b)) -> (A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k) -> (z = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c)))))
114	113	imp 418	. . . . . . . . . . . . 13 |- (((k e. Nn /\ (b e. k /\ w e. ∼ b)) /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) -> (z = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))))
115	114	an32s 779	. . . . . . . . . . . 12 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (b e. k /\ w e. ∼ b)) -> (z = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))))
116	115	rexlimdvva 2745	. . . . . . . . . . 11 |- ((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) -> (E.b e. k E.w e. ∼ bz = (b u. {w}) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))))
117	47, 116	syl5bi 208	. . . . . . . . . 10 |- ((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) -> (z e. (k +o 1c) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))))
118	117	imp32 422	. . . . . . . . 9 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (z e. (k +o 1c) /\ z C_ Nn )) -> {a | E.x e. z a = Tfin x} e. ( Tfin k +o 1c))
119		simpll 730	. . . . . . . . . 10 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (z e. (k +o 1c) /\ z C_ Nn )) -> k e. Nn )
120		ne0i 3556	. . . . . . . . . . 11 |- (z e. (k +o 1c) -> (k +o 1c) =/= (/))
121	120	ad2antrl 708	. . . . . . . . . 10 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (z e. (k +o 1c) /\ z C_ Nn )) -> (k +o 1c) =/= (/))
122		tfinsuc 4498	. . . . . . . . . 10 |- ((k e. Nn /\ (k +o 1c) =/= (/)) -> Tfin (k +o 1c) = ( Tfin k +o 1c))
123	119, 121, 122	syl2anc 642	. . . . . . . . 9 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (z e. (k +o 1c) /\ z C_ Nn )) -> Tfin (k +o 1c) = ( Tfin k +o 1c))
124	118, 123	eleqtrrd 2430	. . . . . . . 8 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ (z e. (k +o 1c) /\ z C_ Nn )) -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c))
125	124	expr 598	. . . . . . 7 |- (((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) /\ z e. (k +o 1c)) -> (z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c)))
126	125	ralrimiva 2697	. . . . . 6 |- ((k e. Nn /\ A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k)) -> A.z e. (k +o 1c)(z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c)))
127	126	ex 423	. . . . 5 |- (k e. Nn -> (A.y e. k (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin k) -> A.z e. (k +o 1c)(z C_ Nn -> {a | E.x e. z a = Tfin x} e. Tfin (k +o 1c))))
128	1, 24, 28, 39, 43, 46, 127	finds 4411	. . . 4 |- (N e. Nn -> A.y e. N (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin N))
129		sseq1 3292	. . . . . 6 |- (y = A -> (y C_ Nn <-> A C_ Nn ))
130		rexeq 2808	. . . . . . . 8 |- (y = A -> (E.x e. y a = Tfin x <-> E.x e. A a = Tfin x))
131	130	abbidv 2467	. . . . . . 7 |- (y = A -> {a | E.x e. y a = Tfin x} = {a | E.x e. A a = Tfin x})
132	131	eleq1d 2419	. . . . . 6 |- (y = A -> ({a | E.x e. y a = Tfin x} e. Tfin N <-> {a | E.x e. A a = Tfin x} e. Tfin N))
133	129, 132	imbi12d 311	. . . . 5 |- (y = A -> ((y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin N) <-> (A C_ Nn -> {a | E.x e. A a = Tfin x} e. Tfin N)))
134	133	rspccv 2952	. . . 4 |- (A.y e. N (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin N) -> (A e. N -> (A C_ Nn -> {a | E.x e. A a = Tfin x} e. Tfin N)))
135	128, 134	syl 15	. . 3 |- (N e. Nn -> (A e. N -> (A C_ Nn -> {a | E.x e. A a = Tfin x} e. Tfin N)))
136	135	com23 72	. 2 |- (N e. Nn -> (A C_ Nn -> (A e. N -> {a | E.x e. A a = Tfin x} e. Tfin N)))
137	136	3imp 1145	1 |- ((N e. Nn /\ A C_ Nn /\ A e. N) -> {a | E.x e. A a = Tfin x} e. Tfin N)

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   /\ wa 358   /\ w3a 934  A.wal 1540   = wceq 1642   e. wcel 1710  {cab 2339   =/= wne 2516  A.wral 2614  E.wrex 2615   ∼ ccompl 3205   u. cun 3207   C_ wss 3257  (/)c0 3550  {csn 3737  1_cc1c 4134   Nn cnnc 4373  0_cc0c 4374   +o cplc 4375   T_fin ctfin 4435

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-tfin 4443

This theorem is referenced by:  vfinncsp  4554