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

Theorem vfinspsslem1 4550
Description: Lemma for vfinspss 4551. Establish part of the inductive step. (Contributed by SF, 3-Feb-2015.)
Assertion
Ref Expression
vfinspsslem1 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → x Spfin z = Tfin x)
Distinct variable group:   z,n,x

Proof of Theorem vfinspsslem1
Dummy variables a b p g d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 443 . . . . . 6 ((V Fin n Spfin ) → V Fin )
2 vfinspnn 4541 . . . . . . . 8 (V FinSpfin ( Nn {}))
3 difss 3393 . . . . . . . 8 ( Nn {}) Nn
42, 3syl6ss 3284 . . . . . . 7 (V FinSpfin Nn )
54sselda 3273 . . . . . 6 ((V Fin n Spfin ) → n Nn )
62sselda 3273 . . . . . . 7 ((V Fin n Spfin ) → n ( Nn {}))
7 eldifsn 3839 . . . . . . . 8 (n ( Nn {}) ↔ (n Nn n))
87simprbi 450 . . . . . . 7 (n ( Nn {}) → n)
96, 8syl 15 . . . . . 6 ((V Fin n Spfin ) → n)
10 vfintle 4546 . . . . . 6 ((V Fin n Nn n) → ⟪ Tfin n, Ncfin 1cfin )
111, 5, 9, 10syl3anc 1182 . . . . 5 ((V Fin n Spfin ) → ⟪ Tfin n, Ncfin 1cfin )
1211ad2ant2r 727 . . . 4 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ⟪ Tfin n, Ncfin 1cfin )
13 t1csfin1c 4545 . . . . . . . 8 (V FinSfin ( Tfin Ncfin 1c, Ncfin 1c))
1413adantr 451 . . . . . . 7 ((V Fin Tfin n Spfin ) → Sfin ( Tfin Ncfin 1c, Ncfin 1c))
15 simpr 447 . . . . . . 7 ((n Spfin Sfin (z, Tfin n)) → Sfin (z, Tfin n))
16 sfinltfin 4535 . . . . . . . 8 ((( Sfin ( Tfin Ncfin 1c, Ncfin 1c) Sfin (z, Tfin n)) Tfin Ncfin 1c, z <fin ) → ⟪ Ncfin 1c, Tfin n <fin )
1716ex 423 . . . . . . 7 (( Sfin ( Tfin Ncfin 1c, Ncfin 1c) Sfin (z, Tfin n)) → (⟪ Tfin Ncfin 1c, z <fin → ⟪ Ncfin 1c, Tfin n <fin ))
1814, 15, 17syl2an 463 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (⟪ Tfin Ncfin 1c, z <fin → ⟪ Ncfin 1c, Tfin n <fin ))
1918con3d 125 . . . . 5 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (¬ ⟪ Ncfin 1c, Tfin n <fin → ¬ ⟪ Tfin Ncfin 1c, z <fin ))
205ad2ant2r 727 . . . . . . 7 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → n Nn )
21 tfincl 4492 . . . . . . 7 (n NnTfin n Nn )
2220, 21syl 15 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → Tfin n Nn )
23 1cex 4142 . . . . . . . . 9 1c V
24 ncfinprop 4474 . . . . . . . . 9 ((V Fin 1c V) → ( Ncfin 1c Nn 1c Ncfin 1c))
2523, 24mpan2 652 . . . . . . . 8 (V Fin → ( Ncfin 1c Nn 1c Ncfin 1c))
2625ad2antrr 706 . . . . . . 7 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ( Ncfin 1c Nn 1c Ncfin 1c))
2726simpld 445 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → Ncfin 1c Nn )
28 lenltfin 4469 . . . . . 6 (( Tfin n Nn Ncfin 1c Nn ) → (⟪ Tfin n, Ncfin 1cfin ↔ ¬ ⟪ Ncfin 1c, Tfin n <fin ))
2922, 27, 28syl2anc 642 . . . . 5 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (⟪ Tfin n, Ncfin 1cfin ↔ ¬ ⟪ Ncfin 1c, Tfin n <fin ))
30 df-sfin 4446 . . . . . . . 8 ( Sfin (z, Tfin n) ↔ (z Nn Tfin n Nn a(1a z a Tfin n)))
3130simp1bi 970 . . . . . . 7 ( Sfin (z, Tfin n) → z Nn )
3231ad2antll 709 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → z Nn )
33 tfincl 4492 . . . . . . 7 ( Ncfin 1c NnTfin Ncfin 1c Nn )
3427, 33syl 15 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → Tfin Ncfin 1c Nn )
35 lenltfin 4469 . . . . . 6 ((z Nn Tfin Ncfin 1c Nn ) → (⟪z, Tfin Ncfin 1cfin ↔ ¬ ⟪ Tfin Ncfin 1c, z <fin ))
3632, 34, 35syl2anc 642 . . . . 5 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (⟪z, Tfin Ncfin 1cfin ↔ ¬ ⟪ Tfin Ncfin 1c, z <fin ))
3719, 29, 363imtr4d 259 . . . 4 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (⟪ Tfin n, Ncfin 1cfin → ⟪z, Tfin Ncfin 1cfin ))
3812, 37mpd 14 . . 3 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ⟪z, Tfin Ncfin 1cfin )
39 vex 2862 . . . 4 z V
40 tfinex 4485 . . . 4 Tfin Ncfin 1c V
41 opklefing 4448 . . . 4 ((z V Tfin Ncfin 1c V) → (⟪z, Tfin Ncfin 1cfinp Nn Tfin Ncfin 1c = (z +c p)))
4239, 40, 41mp2an 653 . . 3 (⟪z, Tfin Ncfin 1cfinp Nn Tfin Ncfin 1c = (z +c p))
4338, 42sylib 188 . 2 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → p Nn Tfin Ncfin 1c = (z +c p))
44 df1c2 4168 . . . . . . 7 1c = 1V
45 pw1eq 4143 . . . . . . 7 (1c = 1V → 11c = 11V)
4644, 45ax-mp 5 . . . . . 6 11c = 11V
47 tfinpw1 4494 . . . . . . 7 (( Ncfin 1c Nn 1c Ncfin 1c) → 11c Tfin Ncfin 1c)
4826, 47syl 15 . . . . . 6 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → 11c Tfin Ncfin 1c)
4946, 48syl5eqelr 2438 . . . . 5 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → 11V Tfin Ncfin 1c)
50 eleq2 2414 . . . . 5 ( Tfin Ncfin 1c = (z +c p) → (11V Tfin Ncfin 1c11V (z +c p)))
5149, 50syl5ibcom 211 . . . 4 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ( Tfin Ncfin 1c = (z +c p) → 11V (z +c p)))
52 eladdc 4398 . . . . 5 (11V (z +c p) ↔ a z b p ((ab) = 11V = (ab)))
53 ssun1 3426 . . . . . . . . . . 11 a (ab)
54 sseq2 3293 . . . . . . . . . . 11 (11V = (ab) → (a 11V ↔ a (ab)))
5553, 54mpbiri 224 . . . . . . . . . 10 (11V = (ab) → a 11V)
56 vex 2862 . . . . . . . . . . . 12 a V
5756sspw1 4335 . . . . . . . . . . 11 (a 11V ↔ g(g 1V a = 1g))
58 vex 2862 . . . . . . . . . . . . . . . 16 g V
5958sspw1 4335 . . . . . . . . . . . . . . 15 (g 1V ↔ d(d V g = 1d))
60 ssv 3291 . . . . . . . . . . . . . . . . 17 d V
6160biantrur 492 . . . . . . . . . . . . . . . 16 (g = 1d ↔ (d V g = 1d))
6261exbii 1582 . . . . . . . . . . . . . . 15 (d g = 1dd(d V g = 1d))
6359, 62bitr4i 243 . . . . . . . . . . . . . 14 (g 1V ↔ d g = 1d)
6463anbi1i 676 . . . . . . . . . . . . 13 ((g 1V a = 1g) ↔ (d g = 1d a = 1g))
65 19.41v 1901 . . . . . . . . . . . . 13 (d(g = 1d a = 1g) ↔ (d g = 1d a = 1g))
6664, 65bitr4i 243 . . . . . . . . . . . 12 ((g 1V a = 1g) ↔ d(g = 1d a = 1g))
6766exbii 1582 . . . . . . . . . . 11 (g(g 1V a = 1g) ↔ gd(g = 1d a = 1g))
68 excom 1741 . . . . . . . . . . . 12 (gd(g = 1d a = 1g) ↔ dg(g = 1d a = 1g))
69 vex 2862 . . . . . . . . . . . . . . 15 d V
7069pw1ex 4303 . . . . . . . . . . . . . 14 1d V
71 pw1eq 4143 . . . . . . . . . . . . . . 15 (g = 1d1g = 11d)
7271eqeq2d 2364 . . . . . . . . . . . . . 14 (g = 1d → (a = 1ga = 11d))
7370, 72ceqsexv 2894 . . . . . . . . . . . . 13 (g(g = 1d a = 1g) ↔ a = 11d)
7473exbii 1582 . . . . . . . . . . . 12 (dg(g = 1d a = 1g) ↔ d a = 11d)
7568, 74bitri 240 . . . . . . . . . . 11 (gd(g = 1d a = 1g) ↔ d a = 11d)
7657, 67, 753bitri 262 . . . . . . . . . 10 (a 11V ↔ d a = 11d)
7755, 76sylib 188 . . . . . . . . 9 (11V = (ab) → d a = 11d)
78 eleq1 2413 . . . . . . . . . . . . 13 (a = 11d → (a z11d z))
7978biimpac 472 . . . . . . . . . . . 12 ((a z a = 11d) → 11d z)
8032adantr 451 . . . . . . . . . . . . . . 15 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) 11d z) → z Nn )
81 ncfinprop 4474 . . . . . . . . . . . . . . . . . . . 20 ((V Fin 1d V) → ( Ncfin 1d Nn 1d Ncfin 1d))
8270, 81mpan2 652 . . . . . . . . . . . . . . . . . . 19 (V Fin → ( Ncfin 1d Nn 1d Ncfin 1d))
8382ad2antrr 706 . . . . . . . . . . . . . . . . . 18 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ( Ncfin 1d Nn 1d Ncfin 1d))
8483simpld 445 . . . . . . . . . . . . . . . . 17 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → Ncfin 1d Nn )
85 tfincl 4492 . . . . . . . . . . . . . . . . 17 ( Ncfin 1d NnTfin Ncfin 1d Nn )
8684, 85syl 15 . . . . . . . . . . . . . . . 16 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → Tfin Ncfin 1d Nn )
8786adantr 451 . . . . . . . . . . . . . . 15 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) 11d z) → Tfin Ncfin 1d Nn )
88 simpr 447 . . . . . . . . . . . . . . 15 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) 11d z) → 11d z)
89 tfinpw1 4494 . . . . . . . . . . . . . . . . 17 (( Ncfin 1d Nn 1d Ncfin 1d) → 11d Tfin Ncfin 1d)
9083, 89syl 15 . . . . . . . . . . . . . . . 16 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → 11d Tfin Ncfin 1d)
9190adantr 451 . . . . . . . . . . . . . . 15 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) 11d z) → 11d Tfin Ncfin 1d)
92 nnceleq 4430 . . . . . . . . . . . . . . 15 (((z Nn Tfin Ncfin 1d Nn ) (11d z 11d Tfin Ncfin 1d)) → z = Tfin Ncfin 1d)
9380, 87, 88, 91, 92syl22anc 1183 . . . . . . . . . . . . . 14 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) 11d z) → z = Tfin Ncfin 1d)
9493ex 423 . . . . . . . . . . . . 13 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (11d zz = Tfin Ncfin 1d))
955ad2ant2r 727 . . . . . . . . . . . . . . . . . . 19 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → n Nn )
9669pwex 4329 . . . . . . . . . . . . . . . . . . . . . 22 d V
97 ncfinprop 4474 . . . . . . . . . . . . . . . . . . . . . 22 ((V Fin d V) → ( Ncfin d Nn d Ncfin d))
9896, 97mpan2 652 . . . . . . . . . . . . . . . . . . . . 21 (V Fin → ( Ncfin d Nn d Ncfin d))
9998simpld 445 . . . . . . . . . . . . . . . . . . . 20 (V FinNcfin d Nn )
10099ad2antrr 706 . . . . . . . . . . . . . . . . . . 19 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Ncfin d Nn )
101 simprr 733 . . . . . . . . . . . . . . . . . . . 20 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Sfin ( Tfin Ncfin 1d, Tfin n))
10282simpld 445 . . . . . . . . . . . . . . . . . . . . . . 23 (V FinNcfin 1d Nn )
10382simprd 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (V Fin1d Ncfin 1d)
10498simprd 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (V Find Ncfin d)
105 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a = d1a = 1d)
106105eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a = d → (1a Ncfin 1d1d Ncfin 1d))
107 pweq 3725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a = da = d)
108107eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a = d → (a Ncfin dd Ncfin d))
109106, 108anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a = d → ((1a Ncfin 1d a Ncfin d) ↔ (1d Ncfin 1d d Ncfin d)))
11069, 109spcev 2946 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1d Ncfin 1d d Ncfin d) → a(1a Ncfin 1d a Ncfin d))
111103, 104, 110syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23 (V Fina(1a Ncfin 1d a Ncfin d))
112 df-sfin 4446 . . . . . . . . . . . . . . . . . . . . . . 23 ( Sfin ( Ncfin 1d, Ncfin d) ↔ ( Ncfin 1d Nn Ncfin d Nn a(1a Ncfin 1d a Ncfin d)))
113102, 99, 111, 112syl3anbrc 1136 . . . . . . . . . . . . . . . . . . . . . 22 (V FinSfin ( Ncfin 1d, Ncfin d))
114113ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Sfin ( Ncfin 1d, Ncfin d))
115 sfintfin 4532 . . . . . . . . . . . . . . . . . . . . 21 ( Sfin ( Ncfin 1d, Ncfin d) → Sfin ( Tfin Ncfin 1d, Tfin Ncfin d))
116114, 115syl 15 . . . . . . . . . . . . . . . . . . . 20 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Sfin ( Tfin Ncfin 1d, Tfin Ncfin d))
117 sfin112 4529 . . . . . . . . . . . . . . . . . . . 20 (( Sfin ( Tfin Ncfin 1d, Tfin n) Sfin ( Tfin Ncfin 1d, Tfin Ncfin d)) → Tfin n = Tfin Ncfin d)
118101, 116, 117syl2anc 642 . . . . . . . . . . . . . . . . . . 19 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Tfin n = Tfin Ncfin d)
119 tfin11 4493 . . . . . . . . . . . . . . . . . . 19 ((n Nn Ncfin d Nn Tfin n = Tfin Ncfin d) → n = Ncfin d)
12095, 100, 118, 119syl3anc 1182 . . . . . . . . . . . . . . . . . 18 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → n = Ncfin d)
121 simprl 732 . . . . . . . . . . . . . . . . . 18 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → n Spfin )
122120, 121eqeltrrd 2428 . . . . . . . . . . . . . . . . 17 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Ncfin d Spfin )
123 spfinsfincl 4539 . . . . . . . . . . . . . . . . 17 (( Ncfin d Spfin Sfin ( Ncfin 1d, Ncfin d)) → Ncfin 1d Spfin )
124122, 114, 123syl2anc 642 . . . . . . . . . . . . . . . 16 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → Ncfin 1d Spfin )
125 risset 2661 . . . . . . . . . . . . . . . . 17 ( Ncfin 1d Spfinx Spfin x = Ncfin 1d)
126 tfineq 4488 . . . . . . . . . . . . . . . . . . 19 (x = Ncfin 1dTfin x = Tfin Ncfin 1d)
127126eqcomd 2358 . . . . . . . . . . . . . . . . . 18 (x = Ncfin 1dTfin Ncfin 1d = Tfin x)
128127reximi 2721 . . . . . . . . . . . . . . . . 17 (x Spfin x = Ncfin 1dx Spfin Tfin Ncfin 1d = Tfin x)
129125, 128sylbi 187 . . . . . . . . . . . . . . . 16 ( Ncfin 1d Spfinx Spfin Tfin Ncfin 1d = Tfin x)
130124, 129syl 15 . . . . . . . . . . . . . . 15 (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → x Spfin Tfin Ncfin 1d = Tfin x)
131 sfineq1 4526 . . . . . . . . . . . . . . . . . 18 (z = Tfin Ncfin 1d → ( Sfin (z, Tfin n) ↔ Sfin ( Tfin Ncfin 1d, Tfin n)))
132131anbi2d 684 . . . . . . . . . . . . . . . . 17 (z = Tfin Ncfin 1d → ((n Spfin Sfin (z, Tfin n)) ↔ (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))))
133132anbi2d 684 . . . . . . . . . . . . . . . 16 (z = Tfin Ncfin 1d → (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) ↔ ((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n)))))
134 eqeq1 2359 . . . . . . . . . . . . . . . . 17 (z = Tfin Ncfin 1d → (z = Tfin xTfin Ncfin 1d = Tfin x))
135134rexbidv 2635 . . . . . . . . . . . . . . . 16 (z = Tfin Ncfin 1d → (x Spfin z = Tfin xx Spfin Tfin Ncfin 1d = Tfin x))
136133, 135imbi12d 311 . . . . . . . . . . . . . . 15 (z = Tfin Ncfin 1d → ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → x Spfin z = Tfin x) ↔ (((V Fin Tfin n Spfin ) (n Spfin Sfin ( Tfin Ncfin 1d, Tfin n))) → x Spfin Tfin Ncfin 1d = Tfin x)))
137130, 136mpbiri 224 . . . . . . . . . . . . . 14 (z = Tfin Ncfin 1d → (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → x Spfin z = Tfin x))
138137com12 27 . . . . . . . . . . . . 13 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (z = Tfin Ncfin 1dx Spfin z = Tfin x))
13994, 138syld 40 . . . . . . . . . . . 12 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (11d zx Spfin z = Tfin x))
14079, 139syl5 28 . . . . . . . . . . 11 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ((a z a = 11d) → x Spfin z = Tfin x))
141140expdimp 426 . . . . . . . . . 10 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) a z) → (a = 11dx Spfin z = Tfin x))
142141exlimdv 1636 . . . . . . . . 9 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) a z) → (d a = 11dx Spfin z = Tfin x))
14377, 142syl5 28 . . . . . . . 8 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) a z) → (11V = (ab) → x Spfin z = Tfin x))
144143adantld 453 . . . . . . 7 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) a z) → (((ab) = 11V = (ab)) → x Spfin z = Tfin x))
145144adantrr 697 . . . . . 6 ((((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) (a z b p)) → (((ab) = 11V = (ab)) → x Spfin z = Tfin x))
146145rexlimdvva 2745 . . . . 5 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (a z b p ((ab) = 11V = (ab)) → x Spfin z = Tfin x))
14752, 146syl5bi 208 . . . 4 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (11V (z +c p) → x Spfin z = Tfin x))
14851, 147syld 40 . . 3 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → ( Tfin Ncfin 1c = (z +c p) → x Spfin z = Tfin x))
149148rexlimdvw 2741 . 2 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → (p Nn Tfin Ncfin 1c = (z +c p) → x Spfin z = Tfin x))
15043, 149mpd 14 1 (((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → x Spfin z = Tfin x)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358  wex 1541   = wceq 1642   wcel 1710  wne 2516  wrex 2615  Vcvv 2859   cdif 3206  cun 3207  cin 3208   wss 3257  c0 3550  cpw 3722  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   Nn cnnc 4373   +c cplc 4375   Fin cfin 4376  fin clefin 4432   <fin cltfin 4433   Ncfin cncfin 4434   Tfin ctfin 4435   Sfin wsfin 4438   Spfin cspfin 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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-3or 935  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-pss 3261  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-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-sfin 4446  df-spfin 4447
This theorem is referenced by:  vfinspss  4551
  Copyright terms: Public domain W3C validator