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 e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.x e. 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.

Step	Hyp	Ref	Expression
1		simpl 443	. . . . . 6 |- ((_V e. Fin /\ n e. Spfin ) -> _V e. Fin )
2		vfinspnn 4541	. . . . . . . 8 |- (_V e. Fin -> Spfin C_ ( Nn \ {(/)}))
3		difss 3393	. . . . . . . 8 |- ( Nn \ {(/)}) C_ Nn
4	2, 3	syl6ss 3284	. . . . . . 7 |- (_V e. Fin -> Spfin C_ Nn )
5	4	sselda 3273	. . . . . 6 |- ((_V e. Fin /\ n e. Spfin ) -> n e. Nn )
6	2	sselda 3273	. . . . . . 7 |- ((_V e. Fin /\ n e. Spfin ) -> n e. ( Nn \ {(/)}))
7		eldifsn 3839	. . . . . . . 8 |- (n e. ( Nn \ {(/)}) <-> (n e. Nn /\ n =/= (/)))
8	7	simprbi 450	. . . . . . 7 |- (n e. ( Nn \ {(/)}) -> n =/= (/))
9	6, 8	syl 15	. . . . . 6 |- ((_V e. Fin /\ n e. Spfin ) -> n =/= (/))
10		vfintle 4546	. . . . . 6 |- ((_V e. Fin /\ n e. Nn /\ n =/= (/)) -> << Tfin n, Ncfin 1c>> e. <_fin )
11	1, 5, 9, 10	syl3anc 1182	. . . . 5 |- ((_V e. Fin /\ n e. Spfin ) -> << Tfin n, Ncfin 1c>> e. <_fin )
12	11	ad2ant2r 727	. . . 4 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> << Tfin n, Ncfin 1c>> e. <_fin )
13		t1csfin1c 4545	. . . . . . . 8 |- (_V e. Fin -> Sfin ( Tfin Ncfin 1c, Ncfin 1c))
14	13	adantr 451	. . . . . . 7 |- ((_V e. Fin /\ Tfin n e. Spfin ) -> Sfin ( Tfin Ncfin 1c, Ncfin 1c))
15		simpr 447	. . . . . . 7 |- ((n e. 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>> e. <fin ) -> << Ncfin 1c, Tfin n>> e. <fin )
17	16	ex 423	. . . . . . 7 |- (( Sfin ( Tfin Ncfin 1c, Ncfin 1c) /\ Sfin (z, Tfin n)) -> (<< Tfin Ncfin 1c, z>> e. <fin -> << Ncfin 1c, Tfin n>> e. <fin ))
18	14, 15, 17	syl2an 463	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (<< Tfin Ncfin 1c, z>> e. <fin -> << Ncfin 1c, Tfin n>> e. <fin ))
19	18	con3d 125	. . . . 5 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (-. << Ncfin 1c, Tfin n>> e. <fin -> -. << Tfin Ncfin 1c, z>> e. <fin ))
20	5	ad2ant2r 727	. . . . . . 7 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> n e. Nn )
21		tfincl 4492	. . . . . . 7 |- (n e. Nn -> Tfin n e. Nn )
22	20, 21	syl 15	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> Tfin n e. Nn )
23		1cex 4142	. . . . . . . . 9 |- 1c e. _V
24		ncfinprop 4474	. . . . . . . . 9 |- ((_V e. Fin /\ 1c e. _V) -> ( Ncfin 1c e. Nn /\ 1c e. Ncfin 1c))
25	23, 24	mpan2 652	. . . . . . . 8 |- (_V e. Fin -> ( Ncfin 1c e. Nn /\ 1c e. Ncfin 1c))
26	25	ad2antrr 706	. . . . . . 7 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ( Ncfin 1c e. Nn /\ 1c e. Ncfin 1c))
27	26	simpld 445	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> Ncfin 1c e. Nn )
28		lenltfin 4469	. . . . . 6 |- (( Tfin n e. Nn /\ Ncfin 1c e. Nn ) -> (<< Tfin n, Ncfin 1c>> e. <_fin <-> -. << Ncfin 1c, Tfin n>> e. <fin ))
29	22, 27, 28	syl2anc 642	. . . . 5 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (<< Tfin n, Ncfin 1c>> e. <_fin <-> -. << Ncfin 1c, Tfin n>> e. <fin ))
30		df-sfin 4446	. . . . . . . 8 |- ( Sfin (z, Tfin n) <-> (z e. Nn /\ Tfin n e. Nn /\ E.a(~P1 a e. z /\ ~Pa e. Tfin n)))
31	30	simp1bi 970	. . . . . . 7 |- ( Sfin (z, Tfin n) -> z e. Nn )
32	31	ad2antll 709	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> z e. Nn )
33		tfincl 4492	. . . . . . 7 |- ( Ncfin 1c e. Nn -> Tfin Ncfin 1c e. Nn )
34	27, 33	syl 15	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> Tfin Ncfin 1c e. Nn )
35		lenltfin 4469	. . . . . 6 |- ((z e. Nn /\ Tfin Ncfin 1c e. Nn ) -> (<<z, Tfin Ncfin 1c>> e. <_fin <-> -. << Tfin Ncfin 1c, z>> e. <fin ))
36	32, 34, 35	syl2anc 642	. . . . 5 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (<<z, Tfin Ncfin 1c>> e. <_fin <-> -. << Tfin Ncfin 1c, z>> e. <fin ))
37	19, 29, 36	3imtr4d 259	. . . 4 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (<< Tfin n, Ncfin 1c>> e. <_fin -> <<z, Tfin Ncfin 1c>> e. <_fin ))
38	12, 37	mpd 14	. . 3 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> <<z, Tfin Ncfin 1c>> e. <_fin )
39		vex 2862	. . . 4 |- z e. _V
40		tfinex 4485	. . . 4 |- Tfin Ncfin 1c e. _V
41		opklefing 4448	. . . 4 |- ((z e. _V /\ Tfin Ncfin 1c e. _V) -> (<<z, Tfin Ncfin 1c>> e. <_fin <-> E.p e. Nn Tfin Ncfin 1c = (z +o p)))
42	39, 40, 41	mp2an 653	. . 3 |- (<<z, Tfin Ncfin 1c>> e. <_fin <-> E.p e. Nn Tfin Ncfin 1c = (z +o p))
43	38, 42	sylib 188	. 2 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.p e. Nn Tfin Ncfin 1c = (z +o p))
44		df1c2 4168	. . . . . . 7 |- 1c = ~P1 _V
45		pw1eq 4143	. . . . . . 7 |- (1c = ~P1 _V -> ~P1 1c = ~P1 ~P1 _V)
46	44, 45	ax-mp 5	. . . . . 6 |- ~P1 1c = ~P1 ~P1 _V
47		tfinpw1 4494	. . . . . . 7 |- (( Ncfin 1c e. Nn /\ 1c e. Ncfin 1c) -> ~P1 1c e. Tfin Ncfin 1c)
48	26, 47	syl 15	. . . . . 6 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ~P1 1c e. Tfin Ncfin 1c)
49	46, 48	syl5eqelr 2438	. . . . 5 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ~P1 ~P1 _V e. Tfin Ncfin 1c)
50		eleq2 2414	. . . . 5 |- ( Tfin Ncfin 1c = (z +o p) -> (~P1 ~P1 _V e. Tfin Ncfin 1c <-> ~P1 ~P1 _V e. (z +o p)))
51	49, 50	syl5ibcom 211	. . . 4 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ( Tfin Ncfin 1c = (z +o p) -> ~P1 ~P1 _V e. (z +o p)))
52		eladdc 4398	. . . . 5 |- (~P1 ~P1 _V e. (z +o p) <-> E.a e. z E.b e. p ((a i^i b) = (/) /\ ~P1 ~P1 _V = (a u. b)))
53		ssun1 3426	. . . . . . . . . . 11 |- a C_ (a u. b)
54		sseq2 3293	. . . . . . . . . . 11 |- (~P1 ~P1 _V = (a u. b) -> (a C_ ~P1 ~P1 _V <-> a C_ (a u. b)))
55	53, 54	mpbiri 224	. . . . . . . . . 10 |- (~P1 ~P1 _V = (a u. b) -> a C_ ~P1 ~P1 _V)
56		vex 2862	. . . . . . . . . . . 12 |- a e. _V
57	56	sspw1 4335	. . . . . . . . . . 11 |- (a C_ ~P1 ~P1 _V <-> E.g(g C_ ~P1 _V /\ a = ~P1 g))
58		vex 2862	. . . . . . . . . . . . . . . 16 |- g e. _V
59	58	sspw1 4335	. . . . . . . . . . . . . . 15 |- (g C_ ~P1 _V <-> E.d(d C_ _V /\ g = ~P1 d))
60		ssv 3291	. . . . . . . . . . . . . . . . 17 |- d C_ _V
61	60	biantrur 492	. . . . . . . . . . . . . . . 16 |- (g = ~P1 d <-> (d C_ _V /\ g = ~P1 d))
62	61	exbii 1582	. . . . . . . . . . . . . . 15 |- (E.d g = ~P1 d <-> E.d(d C_ _V /\ g = ~P1 d))
63	59, 62	bitr4i 243	. . . . . . . . . . . . . 14 |- (g C_ ~P1 _V <-> E.d g = ~P1 d)
64	63	anbi1i 676	. . . . . . . . . . . . 13 |- ((g C_ ~P1 _V /\ a = ~P1 g) <-> (E.d g = ~P1 d /\ a = ~P1 g))
65		19.41v 1901	. . . . . . . . . . . . 13 |- (E.d(g = ~P1 d /\ a = ~P1 g) <-> (E.d g = ~P1 d /\ a = ~P1 g))
66	64, 65	bitr4i 243	. . . . . . . . . . . 12 |- ((g C_ ~P1 _V /\ a = ~P1 g) <-> E.d(g = ~P1 d /\ a = ~P1 g))
67	66	exbii 1582	. . . . . . . . . . 11 |- (E.g(g C_ ~P1 _V /\ a = ~P1 g) <-> E.gE.d(g = ~P1 d /\ a = ~P1 g))
68		excom 1741	. . . . . . . . . . . 12 |- (E.gE.d(g = ~P1 d /\ a = ~P1 g) <-> E.dE.g(g = ~P1 d /\ a = ~P1 g))
69		vex 2862	. . . . . . . . . . . . . . 15 |- d e. _V
70	69	pw1ex 4303	. . . . . . . . . . . . . 14 |- ~P1 d e. _V
71		pw1eq 4143	. . . . . . . . . . . . . . 15 |- (g = ~P1 d -> ~P1 g = ~P1 ~P1 d)
72	71	eqeq2d 2364	. . . . . . . . . . . . . 14 |- (g = ~P1 d -> (a = ~P1 g <-> a = ~P1 ~P1 d))
73	70, 72	ceqsexv 2894	. . . . . . . . . . . . 13 |- (E.g(g = ~P1 d /\ a = ~P1 g) <-> a = ~P1 ~P1 d)
74	73	exbii 1582	. . . . . . . . . . . 12 |- (E.dE.g(g = ~P1 d /\ a = ~P1 g) <-> E.d a = ~P1 ~P1 d)
75	68, 74	bitri 240	. . . . . . . . . . 11 |- (E.gE.d(g = ~P1 d /\ a = ~P1 g) <-> E.d a = ~P1 ~P1 d)
76	57, 67, 75	3bitri 262	. . . . . . . . . 10 |- (a C_ ~P1 ~P1 _V <-> E.d a = ~P1 ~P1 d)
77	55, 76	sylib 188	. . . . . . . . 9 |- (~P1 ~P1 _V = (a u. b) -> E.d a = ~P1 ~P1 d)
78		eleq1 2413	. . . . . . . . . . . . 13 |- (a = ~P1 ~P1 d -> (a e. z <-> ~P1 ~P1 d e. z))
79	78	biimpac 472	. . . . . . . . . . . 12 |- ((a e. z /\ a = ~P1 ~P1 d) -> ~P1 ~P1 d e. z)
80	32	adantr 451	. . . . . . . . . . . . . . 15 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ ~P1 ~P1 d e. z) -> z e. Nn )
81		ncfinprop 4474	. . . . . . . . . . . . . . . . . . . 20 |- ((_V e. Fin /\ ~P1 d e. _V) -> ( Ncfin ~P1 d e. Nn /\ ~P1 d e. Ncfin ~P1 d))
82	70, 81	mpan2 652	. . . . . . . . . . . . . . . . . . 19 |- (_V e. Fin -> ( Ncfin ~P1 d e. Nn /\ ~P1 d e. Ncfin ~P1 d))
83	82	ad2antrr 706	. . . . . . . . . . . . . . . . . 18 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ( Ncfin ~P1 d e. Nn /\ ~P1 d e. Ncfin ~P1 d))
84	83	simpld 445	. . . . . . . . . . . . . . . . 17 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> Ncfin ~P1 d e. Nn )
85		tfincl 4492	. . . . . . . . . . . . . . . . 17 |- ( Ncfin ~P1 d e. Nn -> Tfin Ncfin ~P1 d e. Nn )
86	84, 85	syl 15	. . . . . . . . . . . . . . . 16 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> Tfin Ncfin ~P1 d e. Nn )
87	86	adantr 451	. . . . . . . . . . . . . . 15 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ ~P1 ~P1 d e. z) -> Tfin Ncfin ~P1 d e. Nn )
88		simpr 447	. . . . . . . . . . . . . . 15 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ ~P1 ~P1 d e. z) -> ~P1 ~P1 d e. z)
89		tfinpw1 4494	. . . . . . . . . . . . . . . . 17 |- (( Ncfin ~P1 d e. Nn /\ ~P1 d e. Ncfin ~P1 d) -> ~P1 ~P1 d e. Tfin Ncfin ~P1 d)
90	83, 89	syl 15	. . . . . . . . . . . . . . . 16 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ~P1 ~P1 d e. Tfin Ncfin ~P1 d)
91	90	adantr 451	. . . . . . . . . . . . . . 15 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ ~P1 ~P1 d e. z) -> ~P1 ~P1 d e. Tfin Ncfin ~P1 d)
92		nnceleq 4430	. . . . . . . . . . . . . . 15 |- (((z e. Nn /\ Tfin Ncfin ~P1 d e. Nn ) /\ (~P1 ~P1 d e. z /\ ~P1 ~P1 d e. Tfin Ncfin ~P1 d)) -> z = Tfin Ncfin ~P1 d)
93	80, 87, 88, 91, 92	syl22anc 1183	. . . . . . . . . . . . . 14 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ ~P1 ~P1 d e. z) -> z = Tfin Ncfin ~P1 d)
94	93	ex 423	. . . . . . . . . . . . 13 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (~P1 ~P1 d e. z -> z = Tfin Ncfin ~P1 d))
95	5	ad2ant2r 727	. . . . . . . . . . . . . . . . . . 19 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> n e. Nn )
96	69	pwex 4329	. . . . . . . . . . . . . . . . . . . . . 22 |- ~Pd e. _V
97		ncfinprop 4474	. . . . . . . . . . . . . . . . . . . . . 22 |- ((_V e. Fin /\ ~Pd e. _V) -> ( Ncfin ~Pd e. Nn /\ ~Pd e. Ncfin ~Pd))
98	96, 97	mpan2 652	. . . . . . . . . . . . . . . . . . . . 21 |- (_V e. Fin -> ( Ncfin ~Pd e. Nn /\ ~Pd e. Ncfin ~Pd))
99	98	simpld 445	. . . . . . . . . . . . . . . . . . . 20 |- (_V e. Fin -> Ncfin ~Pd e. Nn )
100	99	ad2antrr 706	. . . . . . . . . . . . . . . . . . 19 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Ncfin ~Pd e. Nn )
101		simprr 733	. . . . . . . . . . . . . . . . . . . 20 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Sfin ( Tfin Ncfin ~P1 d, Tfin n))
102	82	simpld 445	. . . . . . . . . . . . . . . . . . . . . . 23 |- (_V e. Fin -> Ncfin ~P1 d e. Nn )
103	82	simprd 449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (_V e. Fin -> ~P1 d e. Ncfin ~P1 d)
104	98	simprd 449	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (_V e. Fin -> ~Pd e. Ncfin ~Pd)
105		pw1eq 4143	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a = d -> ~P1 a = ~P1 d)
106	105	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = d -> (~P1 a e. Ncfin ~P1 d <-> ~P1 d e. Ncfin ~P1 d))
107		pweq 3725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a = d -> ~Pa = ~Pd)
108	107	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = d -> (~Pa e. Ncfin ~Pd <-> ~Pd e. Ncfin ~Pd))
109	106, 108	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a = d -> ((~P1 a e. Ncfin ~P1 d /\ ~Pa e. Ncfin ~Pd) <-> (~P1 d e. Ncfin ~P1 d /\ ~Pd e. Ncfin ~Pd)))
110	69, 109	spcev 2946	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((~P1 d e. Ncfin ~P1 d /\ ~Pd e. Ncfin ~Pd) -> E.a(~P1 a e. Ncfin ~P1 d /\ ~Pa e. Ncfin ~Pd))
111	103, 104, 110	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . 23 |- (_V e. Fin -> E.a(~P1 a e. Ncfin ~P1 d /\ ~Pa e. Ncfin ~Pd))
112		df-sfin 4446	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Sfin ( Ncfin ~P1 d, Ncfin ~Pd) <-> ( Ncfin ~P1 d e. Nn /\ Ncfin ~Pd e. Nn /\ E.a(~P1 a e. Ncfin ~P1 d /\ ~Pa e. Ncfin ~Pd)))
113	102, 99, 111, 112	syl3anbrc 1136	. . . . . . . . . . . . . . . . . . . . . 22 |- (_V e. Fin -> Sfin ( Ncfin ~P1 d, Ncfin ~Pd))
114	113	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . 21 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Sfin ( Ncfin ~P1 d, Ncfin ~Pd))
115		sfintfin 4532	. . . . . . . . . . . . . . . . . . . . 21 |- ( Sfin ( Ncfin ~P1 d, Ncfin ~Pd) -> Sfin ( Tfin Ncfin ~P1 d, Tfin Ncfin ~Pd))
116	114, 115	syl 15	. . . . . . . . . . . . . . . . . . . 20 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Sfin ( Tfin Ncfin ~P1 d, Tfin Ncfin ~Pd))
117		sfin112 4529	. . . . . . . . . . . . . . . . . . . 20 |- (( Sfin ( Tfin Ncfin ~P1 d, Tfin n) /\ Sfin ( Tfin Ncfin ~P1 d, Tfin Ncfin ~Pd)) -> Tfin n = Tfin Ncfin ~Pd)
118	101, 116, 117	syl2anc 642	. . . . . . . . . . . . . . . . . . 19 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Tfin n = Tfin Ncfin ~Pd)
119		tfin11 4493	. . . . . . . . . . . . . . . . . . 19 |- ((n e. Nn /\ Ncfin ~Pd e. Nn /\ Tfin n = Tfin Ncfin ~Pd) -> n = Ncfin ~Pd)
120	95, 100, 118, 119	syl3anc 1182	. . . . . . . . . . . . . . . . . 18 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> n = Ncfin ~Pd)
121		simprl 732	. . . . . . . . . . . . . . . . . 18 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> n e. Spfin )
122	120, 121	eqeltrrd 2428	. . . . . . . . . . . . . . . . 17 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Ncfin ~Pd e. Spfin )
123		spfinsfincl 4539	. . . . . . . . . . . . . . . . 17 |- (( Ncfin ~Pd e. Spfin /\ Sfin ( Ncfin ~P1 d, Ncfin ~Pd)) -> Ncfin ~P1 d e. Spfin )
124	122, 114, 123	syl2anc 642	. . . . . . . . . . . . . . . 16 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> Ncfin ~P1 d e. Spfin )
125		risset 2661	. . . . . . . . . . . . . . . . 17 |- ( Ncfin ~P1 d e. Spfin <-> E.x e. Spfin x = Ncfin ~P1 d)
126		tfineq 4488	. . . . . . . . . . . . . . . . . . 19 |- (x = Ncfin ~P1 d -> Tfin x = Tfin Ncfin ~P1 d)
127	126	eqcomd 2358	. . . . . . . . . . . . . . . . . 18 |- (x = Ncfin ~P1 d -> Tfin Ncfin ~P1 d = Tfin x)
128	127	reximi 2721	. . . . . . . . . . . . . . . . 17 |- (E.x e. Spfin x = Ncfin ~P1 d -> E.x e. Spfin Tfin Ncfin ~P1 d = Tfin x)
129	125, 128	sylbi 187	. . . . . . . . . . . . . . . 16 |- ( Ncfin ~P1 d e. Spfin -> E.x e. Spfin Tfin Ncfin ~P1 d = Tfin x)
130	124, 129	syl 15	. . . . . . . . . . . . . . 15 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> E.x e. Spfin Tfin Ncfin ~P1 d = Tfin x)
131		sfineq1 4526	. . . . . . . . . . . . . . . . . 18 |- (z = Tfin Ncfin ~P1 d -> ( Sfin (z, Tfin n) <-> Sfin ( Tfin Ncfin ~P1 d, Tfin n)))
132	131	anbi2d 684	. . . . . . . . . . . . . . . . 17 |- (z = Tfin Ncfin ~P1 d -> ((n e. Spfin /\ Sfin (z, Tfin n)) <-> (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))))
133	132	anbi2d 684	. . . . . . . . . . . . . . . 16 |- (z = Tfin Ncfin ~P1 d -> (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) <-> ((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n)))))
134		eqeq1 2359	. . . . . . . . . . . . . . . . 17 |- (z = Tfin Ncfin ~P1 d -> (z = Tfin x <-> Tfin Ncfin ~P1 d = Tfin x))
135	134	rexbidv 2635	. . . . . . . . . . . . . . . 16 |- (z = Tfin Ncfin ~P1 d -> (E.x e. Spfin z = Tfin x <-> E.x e. Spfin Tfin Ncfin ~P1 d = Tfin x))
136	133, 135	imbi12d 311	. . . . . . . . . . . . . . 15 |- (z = Tfin Ncfin ~P1 d -> ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.x e. Spfin z = Tfin x) <-> (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin ( Tfin Ncfin ~P1 d, Tfin n))) -> E.x e. Spfin Tfin Ncfin ~P1 d = Tfin x)))
137	130, 136	mpbiri 224	. . . . . . . . . . . . . 14 |- (z = Tfin Ncfin ~P1 d -> (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.x e. Spfin z = Tfin x))
138	137	com12 27	. . . . . . . . . . . . 13 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (z = Tfin Ncfin ~P1 d -> E.x e. Spfin z = Tfin x))
139	94, 138	syld 40	. . . . . . . . . . . 12 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (~P1 ~P1 d e. z -> E.x e. Spfin z = Tfin x))
140	79, 139	syl5 28	. . . . . . . . . . 11 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ((a e. z /\ a = ~P1 ~P1 d) -> E.x e. Spfin z = Tfin x))
141	140	expdimp 426	. . . . . . . . . 10 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ a e. z) -> (a = ~P1 ~P1 d -> E.x e. Spfin z = Tfin x))
142	141	exlimdv 1636	. . . . . . . . 9 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ a e. z) -> (E.d a = ~P1 ~P1 d -> E.x e. Spfin z = Tfin x))
143	77, 142	syl5 28	. . . . . . . 8 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ a e. z) -> (~P1 ~P1 _V = (a u. b) -> E.x e. Spfin z = Tfin x))
144	143	adantld 453	. . . . . . 7 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ a e. z) -> (((a i^i b) = (/) /\ ~P1 ~P1 _V = (a u. b)) -> E.x e. Spfin z = Tfin x))
145	144	adantrr 697	. . . . . 6 |- ((((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) /\ (a e. z /\ b e. p)) -> (((a i^i b) = (/) /\ ~P1 ~P1 _V = (a u. b)) -> E.x e. Spfin z = Tfin x))
146	145	rexlimdvva 2745	. . . . 5 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (E.a e. z E.b e. p ((a i^i b) = (/) /\ ~P1 ~P1 _V = (a u. b)) -> E.x e. Spfin z = Tfin x))
147	52, 146	syl5bi 208	. . . 4 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (~P1 ~P1 _V e. (z +o p) -> E.x e. Spfin z = Tfin x))
148	51, 147	syld 40	. . 3 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> ( Tfin Ncfin 1c = (z +o p) -> E.x e. Spfin z = Tfin x))
149	148	rexlimdvw 2741	. 2 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> (E.p e. Nn Tfin Ncfin 1c = (z +o p) -> E.x e. Spfin z = Tfin x))
150	43, 149	mpd 14	1 |- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.x e. Spfin z = Tfin x)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710   =/= wne 2516  E.wrex 2615  _Vcvv 2859   \ cdif 3206   u. cun 3207   i^i cin 3208   C_ wss 3257  (/)c0 3550  ~Pcpw 3722  {csn 3737  <<copk 4057  1_cc1c 4134  ~P₁ cpw1 4135   Nn cnnc 4373   +o cplc 4375   Fin cfin 4376   <__fin clefin 4432   <_fin cltfin 4433   Nc_fin cncfin 4434   T_fin ctfin 4435   S_fin wsfin 4438   Sp_fin 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