New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  tfinnn GIF version

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 Nn A Nn A N) → {a x A a = Tfin x} 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.
StepHypRef Expression
1 tfinnnlem1 4533 . . . . 5 {n y n (y Nn → {a x y a = Tfin x} Tfin n)} V
2 tfineq 4488 . . . . . . . . . 10 (n = 0cTfin n = Tfin 0c)
3 tfin0c 4497 . . . . . . . . . 10 Tfin 0c = 0c
42, 3syl6eq 2401 . . . . . . . . 9 (n = 0cTfin n = 0c)
54eleq2d 2420 . . . . . . . 8 (n = 0c → ({a x y a = Tfin x} Tfin n ↔ {a x y a = Tfin x} 0c))
65imbi2d 307 . . . . . . 7 (n = 0c → ((y Nn → {a x y a = Tfin x} Tfin n) ↔ (y Nn → {a x y a = Tfin x} 0c)))
76raleqbi1dv 2815 . . . . . 6 (n = 0c → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ y 0c (y Nn → {a x y a = Tfin x} 0c)))
8 df-ral 2619 . . . . . . 7 (y 0c (y Nn → {a x y a = Tfin x} 0c) ↔ y(y 0c → (y Nn → {a x y a = Tfin x} 0c)))
9 el0c 4421 . . . . . . . . 9 (y 0cy = )
10 el0c 4421 . . . . . . . . . . 11 ({a x y a = Tfin x} 0c ↔ {a x y a = Tfin x} = )
11 ab0 3569 . . . . . . . . . . 11 ({a x y a = Tfin x} = a ¬ x y a = Tfin x)
1210, 11bitri 240 . . . . . . . . . 10 ({a x y a = Tfin x} 0ca ¬ x y a = Tfin x)
1312imbi2i 303 . . . . . . . . 9 ((y Nn → {a x y a = Tfin x} 0c) ↔ (y Nna ¬ x y a = Tfin x))
149, 13imbi12i 316 . . . . . . . 8 ((y 0c → (y Nn → {a x y a = Tfin x} 0c)) ↔ (y = → (y Nna ¬ x y a = Tfin x)))
1514albii 1566 . . . . . . 7 (y(y 0c → (y Nn → {a x y a = Tfin x} 0c)) ↔ y(y = → (y Nna ¬ x y a = Tfin x)))
16 0ex 4110 . . . . . . . 8 V
17 sseq1 3292 . . . . . . . . 9 (y = → (y Nn Nn ))
18 rexeq 2808 . . . . . . . . . . 11 (y = → (x y a = Tfin xx a = Tfin x))
1918notbid 285 . . . . . . . . . 10 (y = → (¬ x y a = Tfin x ↔ ¬ x a = Tfin x))
2019albidv 1625 . . . . . . . . 9 (y = → (a ¬ x y a = Tfin xa ¬ x a = Tfin x))
2117, 20imbi12d 311 . . . . . . . 8 (y = → ((y Nna ¬ x y a = Tfin x) ↔ ( Nna ¬ x a = Tfin x)))
2216, 21ceqsalv 2885 . . . . . . 7 (y(y = → (y Nna ¬ x y a = Tfin x)) ↔ ( Nna ¬ x a = Tfin x))
238, 15, 223bitri 262 . . . . . 6 (y 0c (y Nn → {a x y a = Tfin x} 0c) ↔ ( Nna ¬ x a = Tfin x))
247, 23syl6bb 252 . . . . 5 (n = 0c → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ ( Nna ¬ x a = Tfin x)))
25 tfineq 4488 . . . . . . . 8 (n = kTfin n = Tfin k)
2625eleq2d 2420 . . . . . . 7 (n = k → ({a x y a = Tfin x} Tfin n ↔ {a x y a = Tfin x} Tfin k))
2726imbi2d 307 . . . . . 6 (n = k → ((y Nn → {a x y a = Tfin x} Tfin n) ↔ (y Nn → {a x y a = Tfin x} Tfin k)))
2827raleqbi1dv 2815 . . . . 5 (n = k → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ y k (y Nn → {a x y a = Tfin x} Tfin k)))
29 tfineq 4488 . . . . . . . . 9 (n = (k +c 1c) → Tfin n = Tfin (k +c 1c))
3029eleq2d 2420 . . . . . . . 8 (n = (k +c 1c) → ({a x y a = Tfin x} Tfin n ↔ {a x y a = Tfin x} Tfin (k +c 1c)))
3130imbi2d 307 . . . . . . 7 (n = (k +c 1c) → ((y Nn → {a x y a = Tfin x} Tfin n) ↔ (y Nn → {a x y a = Tfin x} Tfin (k +c 1c))))
3231raleqbi1dv 2815 . . . . . 6 (n = (k +c 1c) → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ y (k +c 1c)(y Nn → {a x y a = Tfin x} Tfin (k +c 1c))))
33 sseq1 3292 . . . . . . . 8 (y = z → (y Nnz Nn ))
34 rexeq 2808 . . . . . . . . . 10 (y = z → (x y a = Tfin xx z a = Tfin x))
3534abbidv 2467 . . . . . . . . 9 (y = z → {a x y a = Tfin x} = {a x z a = Tfin x})
3635eleq1d 2419 . . . . . . . 8 (y = z → ({a x y a = Tfin x} Tfin (k +c 1c) ↔ {a x z a = Tfin x} Tfin (k +c 1c)))
3733, 36imbi12d 311 . . . . . . 7 (y = z → ((y Nn → {a x y a = Tfin x} Tfin (k +c 1c)) ↔ (z Nn → {a x z a = Tfin x} Tfin (k +c 1c))))
3837cbvralv 2835 . . . . . 6 (y (k +c 1c)(y Nn → {a x y a = Tfin x} Tfin (k +c 1c)) ↔ z (k +c 1c)(z Nn → {a x z a = Tfin x} Tfin (k +c 1c)))
3932, 38syl6bb 252 . . . . 5 (n = (k +c 1c) → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ z (k +c 1c)(z Nn → {a x z a = Tfin x} Tfin (k +c 1c))))
40 tfineq 4488 . . . . . . . 8 (n = NTfin n = Tfin N)
4140eleq2d 2420 . . . . . . 7 (n = N → ({a x y a = Tfin x} Tfin n ↔ {a x y a = Tfin x} Tfin N))
4241imbi2d 307 . . . . . 6 (n = N → ((y Nn → {a x y a = Tfin x} Tfin n) ↔ (y Nn → {a x y a = Tfin x} Tfin N)))
4342raleqbi1dv 2815 . . . . 5 (n = N → (y n (y Nn → {a x y a = Tfin x} Tfin n) ↔ y N (y Nn → {a x y a = Tfin x} Tfin N)))
44 rex0 3563 . . . . . . 7 ¬ x a = Tfin x
4544ax-gen 1546 . . . . . 6 a ¬ x a = Tfin x
4645a1i 10 . . . . 5 ( Nna ¬ x a = Tfin x)
47 elsuc 4413 . . . . . . . . . . 11 (z (k +c 1c) ↔ b k w bz = (b ∪ {w}))
48 sseq1 3292 . . . . . . . . . . . . . . . . . 18 (y = b → (y Nnb Nn ))
49 rexeq 2808 . . . . . . . . . . . . . . . . . . . 20 (y = b → (x y a = Tfin xx b a = Tfin x))
5049abbidv 2467 . . . . . . . . . . . . . . . . . . 19 (y = b → {a x y a = Tfin x} = {a x b a = Tfin x})
5150eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (y = b → ({a x y a = Tfin x} Tfin k ↔ {a x b a = Tfin x} Tfin k))
5248, 51imbi12d 311 . . . . . . . . . . . . . . . . 17 (y = b → ((y Nn → {a x y a = Tfin x} Tfin k) ↔ (b Nn → {a x b a = Tfin x} Tfin k)))
5352rspcv 2951 . . . . . . . . . . . . . . . 16 (b k → (y k (y Nn → {a x y a = Tfin x} Tfin k) → (b Nn → {a x b a = Tfin x} Tfin k)))
5453ad2antrl 708 . . . . . . . . . . . . . . 15 ((k Nn (b k w b)) → (y k (y Nn → {a x y a = Tfin x} Tfin k) → (b Nn → {a x b a = Tfin x} Tfin k)))
55 simprl 732 . . . . . . . . . . . . . . . . . . 19 (((k Nn (b k w b)) (b Nn w Nn )) → b Nn )
56 simp3 957 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn (b k w b)) (b Nn w Nn ) {a x b a = Tfin x} Tfin k) → {a x b a = Tfin x} Tfin k)
57 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((k Nn (b k w b)) (b Nn w Nn )) → w b)
58 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 w V
5958elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (w b ↔ ¬ w b)
6057, 59sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((k Nn (b k w b)) (b Nn w Nn )) → ¬ w b)
61 elequ1 1713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (w = x → (w bx b))
6261notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (w = x → (¬ w b ↔ ¬ x b))
6360, 62syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (b k w b)) (b Nn w Nn )) → (w = x → ¬ x b))
6463con2d 107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((k Nn (b k w b)) (b Nn w Nn )) → (x b → ¬ w = x))
6564imp 418 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((k Nn (b k w b)) (b Nn w Nn )) x b) → ¬ w = x)
66 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → ((k Nn (b k w b)) (b Nn w Nn )))
67 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((k Nn (b k w b)) (b Nn w Nn )) → w Nn )
6866, 67syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → w Nn )
6966, 55syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → b Nn )
70 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → x b)
7169, 70sseldd 3274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → x Nn )
72 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → Tfin w = Tfin x)
73 tfin11 4493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((w Nn x Nn Tfin w = Tfin x) → w = x)
7468, 71, 72, 73syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((k Nn (b k w b)) (b Nn w Nn )) x b) Tfin w = Tfin x) → w = x)
7565, 74mtand 640 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((k Nn (b k w b)) (b Nn w Nn )) x b) → ¬ Tfin w = Tfin x)
7675nrexdv 2717 . . . . . . . . . . . . . . . . . . . . . . 23 (((k Nn (b k w b)) (b Nn w Nn )) → ¬ x b Tfin w = Tfin x)
77763adant3 975 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn (b k w b)) (b Nn w Nn ) {a x b a = Tfin x} Tfin k) → ¬ x b Tfin w = Tfin x)
78 tfinex 4485 . . . . . . . . . . . . . . . . . . . . . . 23 Tfin w V
79 eqeq1 2359 . . . . . . . . . . . . . . . . . . . . . . . 24 (a = Tfin w → (a = Tfin xTfin w = Tfin x))
8079rexbidv 2635 . . . . . . . . . . . . . . . . . . . . . . 23 (a = Tfin w → (x b a = Tfin xx b Tfin w = Tfin x))
8178, 80elab 2985 . . . . . . . . . . . . . . . . . . . . . 22 ( Tfin w {a x b a = Tfin x} ↔ x b Tfin w = Tfin x)
8277, 81sylnibr 296 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn (b k w b)) (b Nn w Nn ) {a x b a = Tfin x} Tfin k) → ¬ Tfin w {a x b a = Tfin x})
8378elsuci 4414 . . . . . . . . . . . . . . . . . . . . 21 (({a x b a = Tfin x} Tfin k ¬ Tfin w {a x b a = Tfin x}) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c))
8456, 82, 83syl2anc 642 . . . . . . . . . . . . . . . . . . . 20 (((k Nn (b k w b)) (b Nn w Nn ) {a x b a = Tfin x} Tfin k) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c))
85843expia 1153 . . . . . . . . . . . . . . . . . . 19 (((k Nn (b k w b)) (b Nn w Nn )) → ({a x b a = Tfin x} Tfin k → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c)))
8655, 85embantd 50 . . . . . . . . . . . . . . . . . 18 (((k Nn (b k w b)) (b Nn w Nn )) → ((b Nn → {a x b a = Tfin x} Tfin k) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c)))
8786ex 423 . . . . . . . . . . . . . . . . 17 ((k Nn (b k w b)) → ((b Nn w Nn ) → ((b Nn → {a x b a = Tfin x} Tfin k) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c))))
8887com23 72 . . . . . . . . . . . . . . . 16 ((k Nn (b k w b)) → ((b Nn → {a x b a = Tfin x} Tfin k) → ((b Nn w Nn ) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c))))
89 sseq1 3292 . . . . . . . . . . . . . . . . . . 19 (z = (b ∪ {w}) → (z Nn ↔ (b ∪ {w}) Nn ))
9058snss 3838 . . . . . . . . . . . . . . . . . . . . 21 (w Nn ↔ {w} Nn )
9190anbi2i 675 . . . . . . . . . . . . . . . . . . . 20 ((b Nn w Nn ) ↔ (b Nn {w} Nn ))
92 unss 3437 . . . . . . . . . . . . . . . . . . . 20 ((b Nn {w} Nn ) ↔ (b ∪ {w}) Nn )
9391, 92bitr2i 241 . . . . . . . . . . . . . . . . . . 19 ((b ∪ {w}) Nn ↔ (b Nn w Nn ))
9489, 93syl6bb 252 . . . . . . . . . . . . . . . . . 18 (z = (b ∪ {w}) → (z Nn ↔ (b Nn w Nn )))
95 rexeq 2808 . . . . . . . . . . . . . . . . . . . . . 22 (z = (b ∪ {w}) → (x z a = Tfin xx (b ∪ {w})a = Tfin x))
96 rexun 3443 . . . . . . . . . . . . . . . . . . . . . 22 (x (b ∪ {w})a = Tfin x ↔ (x b a = Tfin x x {w}a = Tfin x))
9795, 96syl6bb 252 . . . . . . . . . . . . . . . . . . . . 21 (z = (b ∪ {w}) → (x z a = Tfin x ↔ (x b a = Tfin x x {w}a = Tfin x)))
9897abbidv 2467 . . . . . . . . . . . . . . . . . . . 20 (z = (b ∪ {w}) → {a x z a = Tfin x} = {a (x b a = Tfin x x {w}a = Tfin x)})
99 df-sn 3741 . . . . . . . . . . . . . . . . . . . . . . 23 { Tfin w} = {a a = Tfin w}
100 tfineq 4488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x = wTfin x = Tfin w)
101100eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x = w → (a = Tfin xa = Tfin w))
10258, 101rexsn 3768 . . . . . . . . . . . . . . . . . . . . . . . 24 (x {w}a = Tfin xa = Tfin w)
103102abbii 2465 . . . . . . . . . . . . . . . . . . . . . . 23 {a x {w}a = Tfin x} = {a a = Tfin w}
10499, 103eqtr4i 2376 . . . . . . . . . . . . . . . . . . . . . 22 { Tfin w} = {a x {w}a = Tfin x}
105104uneq2i 3415 . . . . . . . . . . . . . . . . . . . . 21 ({a x b a = Tfin x} ∪ { Tfin w}) = ({a x b a = Tfin x} ∪ {a x {w}a = Tfin x})
106 unab 3521 . . . . . . . . . . . . . . . . . . . . 21 ({a x b a = Tfin x} ∪ {a x {w}a = Tfin x}) = {a (x b a = Tfin x x {w}a = Tfin x)}
107105, 106eqtr2i 2374 . . . . . . . . . . . . . . . . . . . 20 {a (x b a = Tfin x x {w}a = Tfin x)} = ({a x b a = Tfin x} ∪ { Tfin w})
10898, 107syl6eq 2401 . . . . . . . . . . . . . . . . . . 19 (z = (b ∪ {w}) → {a x z a = Tfin x} = ({a x b a = Tfin x} ∪ { Tfin w}))
109108eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (z = (b ∪ {w}) → ({a x z a = Tfin x} ( Tfin k +c 1c) ↔ ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c)))
11094, 109imbi12d 311 . . . . . . . . . . . . . . . . 17 (z = (b ∪ {w}) → ((z Nn → {a x z a = Tfin x} ( Tfin k +c 1c)) ↔ ((b Nn w Nn ) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c))))
111110biimprcd 216 . . . . . . . . . . . . . . . 16 (((b Nn w Nn ) → ({a x b a = Tfin x} ∪ { Tfin w}) ( Tfin k +c 1c)) → (z = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c))))
11288, 111syl6 29 . . . . . . . . . . . . . . 15 ((k Nn (b k w b)) → ((b Nn → {a x b a = Tfin x} Tfin k) → (z = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c)))))
11354, 112syld 40 . . . . . . . . . . . . . 14 ((k Nn (b k w b)) → (y k (y Nn → {a x y a = Tfin x} Tfin k) → (z = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c)))))
114113imp 418 . . . . . . . . . . . . 13 (((k Nn (b k w b)) y k (y Nn → {a x y a = Tfin x} Tfin k)) → (z = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c))))
115114an32s 779 . . . . . . . . . . . 12 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (b k w b)) → (z = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c))))
116115rexlimdvva 2745 . . . . . . . . . . 11 ((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) → (b k w bz = (b ∪ {w}) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c))))
11747, 116syl5bi 208 . . . . . . . . . 10 ((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) → (z (k +c 1c) → (z Nn → {a x z a = Tfin x} ( Tfin k +c 1c))))
118117imp32 422 . . . . . . . . 9 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (z (k +c 1c) z Nn )) → {a x z a = Tfin x} ( Tfin k +c 1c))
119 simpll 730 . . . . . . . . . 10 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (z (k +c 1c) z Nn )) → k Nn )
120 ne0i 3556 . . . . . . . . . . 11 (z (k +c 1c) → (k +c 1c) ≠ )
121120ad2antrl 708 . . . . . . . . . 10 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (z (k +c 1c) z Nn )) → (k +c 1c) ≠ )
122 tfinsuc 4498 . . . . . . . . . 10 ((k Nn (k +c 1c) ≠ ) → Tfin (k +c 1c) = ( Tfin k +c 1c))
123119, 121, 122syl2anc 642 . . . . . . . . 9 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (z (k +c 1c) z Nn )) → Tfin (k +c 1c) = ( Tfin k +c 1c))
124118, 123eleqtrrd 2430 . . . . . . . 8 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) (z (k +c 1c) z Nn )) → {a x z a = Tfin x} Tfin (k +c 1c))
125124expr 598 . . . . . . 7 (((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) z (k +c 1c)) → (z Nn → {a x z a = Tfin x} Tfin (k +c 1c)))
126125ralrimiva 2697 . . . . . 6 ((k Nn y k (y Nn → {a x y a = Tfin x} Tfin k)) → z (k +c 1c)(z Nn → {a x z a = Tfin x} Tfin (k +c 1c)))
127126ex 423 . . . . 5 (k Nn → (y k (y Nn → {a x y a = Tfin x} Tfin k) → z (k +c 1c)(z Nn → {a x z a = Tfin x} Tfin (k +c 1c))))
1281, 24, 28, 39, 43, 46, 127finds 4411 . . . 4 (N Nny N (y Nn → {a x y a = Tfin x} Tfin N))
129 sseq1 3292 . . . . . 6 (y = A → (y NnA Nn ))
130 rexeq 2808 . . . . . . . 8 (y = A → (x y a = Tfin xx A a = Tfin x))
131130abbidv 2467 . . . . . . 7 (y = A → {a x y a = Tfin x} = {a x A a = Tfin x})
132131eleq1d 2419 . . . . . 6 (y = A → ({a x y a = Tfin x} Tfin N ↔ {a x A a = Tfin x} Tfin N))
133129, 132imbi12d 311 . . . . 5 (y = A → ((y Nn → {a x y a = Tfin x} Tfin N) ↔ (A Nn → {a x A a = Tfin x} Tfin N)))
134133rspccv 2952 . . . 4 (y N (y Nn → {a x y a = Tfin x} Tfin N) → (A N → (A Nn → {a x A a = Tfin x} Tfin N)))
135128, 134syl 15 . . 3 (N Nn → (A N → (A Nn → {a x A a = Tfin x} Tfin N)))
136135com23 72 . 2 (N Nn → (A Nn → (A N → {a x A a = Tfin x} Tfin N)))
1371363imp 1145 1 ((N Nn A Nn A N) → {a x A a = Tfin x} Tfin N)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∀wal 1540   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2516  ∀wral 2614  ∃wrex 2615   ∼ ccompl 3205   ∪ cun 3207   ⊆ wss 3257  ∅c0 3550  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Tfin 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
 Copyright terms: Public domain W3C validator