Theorem nnfoctbdjlem 38293

Description: There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
nnfoctbdjlem.a	|- ( ph -> A C_ NN )
nnfoctbdjlem.g	|- ( ph -> G : A -1-1-onto-> X )
nnfoctbdjlem.dj	|- ( ph -> Disj y e. X y )
nnfoctbdjlem.f	|- F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )

Assertion

Ref	Expression
nnfoctbdjlem	|- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )

Distinct variable groups:   A, n, y   f, F, n   y, F   n, G, y   f, X, n   y, X   ph, n, y

Allowed substitution hints:   ph( f)   A( f)   G( f)

Proof of Theorem nnfoctbdjlem

Dummy variables k x m z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3887	. . . . . . . . 9 |- ( ( n = 1 \/ -. ( n - 1 ) e. A ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
2	1	adantl 468	. . . . . . . 8 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
3		0ex 4535	. . . . . . . . . . 11 |- (/) e. _V
4	3	snid 3996	. . . . . . . . . 10 |- (/) e. { (/) }
5		elun2 3602	. . . . . . . . . 10 |- ( (/) e. { (/) } -> (/) e. ( X u. { (/) } ) )
6	4, 5	ax-mp 5	. . . . . . . . 9 |- (/) e. ( X u. { (/) } )
7	6	a1i 11	. . . . . . . 8 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> (/) e. ( X u. { (/) } ) )
8	2, 7	eqeltrd 2529	. . . . . . 7 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. ( X u. { (/) } ) )
9	8	adantll 720	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. ( X u. { (/) } ) )
10		iffalse 3890	. . . . . . . 8 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
11	10	adantl 468	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
12		nnfoctbdjlem.g	. . . . . . . . . . . 12 |- ( ph -> G : A -1-1-onto-> X )
13		f1of 5814	. . . . . . . . . . . 12 |- ( G : A -1-1-onto-> X -> G : A --> X )
14	12, 13	syl 17	. . . . . . . . . . 11 |- ( ph -> G : A --> X )
15	14	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> G : A --> X )
16		pm2.46 400	. . . . . . . . . . . 12 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) -> -. -. ( n - 1 ) e. A )
17		notnot2 116	. . . . . . . . . . . 12 |- ( -. -. ( n - 1 ) e. A -> ( n - 1 ) e. A )
18	16, 17	syl 17	. . . . . . . . . . 11 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) -> ( n - 1 ) e. A )
19	18	adantl 468	. . . . . . . . . 10 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( n - 1 ) e. A )
20	15, 19	ffvelrnd 6023	. . . . . . . . 9 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. X )
21	20	adantlr 721	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. X )
22		elun1 3601	. . . . . . . 8 |- ( ( G ` ( n - 1 ) ) e. X -> ( G ` ( n - 1 ) ) e. ( X u. { (/) } ) )
23	21, 22	syl 17	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. ( X u. { (/) } ) )
24	11, 23	eqeltrd 2529	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. ( X u. { (/) } ) )
25	9, 24	pm2.61dan 800	. . . . 5 |- ( ( ph /\ n e. NN ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. ( X u. { (/) } ) )
26		nnfoctbdjlem.f	. . . . 5 |- F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
27	25, 26	fmptd 6046	. . . 4 |- ( ph -> F : NN --> ( X u. { (/) } ) )
28		simpr 463	. . . . . . . . . . 11 |- ( ( ph /\ y e. X ) -> y e. X )
29		f1ofo 5821	. . . . . . . . . . . . . 14 |- ( G : A -1-1-onto-> X -> G : A -onto-> X )
30		forn 5796	. . . . . . . . . . . . . 14 |- ( G : A -onto-> X -> ran G = X )
31	12, 29, 30	3syl 18	. . . . . . . . . . . . 13 |- ( ph -> ran G = X )
32	31	eqcomd 2457	. . . . . . . . . . . 12 |- ( ph -> X = ran G )
33	32	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ y e. X ) -> X = ran G )
34	28, 33	eleqtrd 2531	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> y e. ran G )
35	14	ffnd 5729	. . . . . . . . . . . 12 |- ( ph -> G Fn A )
36		fvelrnb 5912	. . . . . . . . . . . 12 |- ( G Fn A -> ( y e. ran G <-> E. k e. A ( G ` k ) = y ) )
37	35, 36	syl 17	. . . . . . . . . . 11 |- ( ph -> ( y e. ran G <-> E. k e. A ( G ` k ) = y ) )
38	37	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> ( y e. ran G <-> E. k e. A ( G ` k ) = y ) )
39	34, 38	mpbid 214	. . . . . . . . 9 |- ( ( ph /\ y e. X ) -> E. k e. A ( G ` k ) = y )
40		nnfoctbdjlem.a	. . . . . . . . . . . . . . . 16 |- ( ph -> A C_ NN )
41	40	sselda 3432	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> k e. NN )
42		peano2nn 10621	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( k + 1 ) e. NN )
43	41, 42	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. A ) -> ( k + 1 ) e. NN )
44	43	3adant3 1028	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( k + 1 ) e. NN )
45	26	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) )
46		1red 9658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 e. RR )
47		1red 9658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> 1 e. RR )
48	41	nnrpd 11339	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> k e. RR+ )
49	47, 48	ltaddrp2d 11372	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. A ) -> 1 < ( k + 1 ) )
50	49	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 < ( k + 1 ) )
51		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = ( k + 1 ) -> n = ( k + 1 ) )
52	51	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( k + 1 ) -> ( k + 1 ) = n )
53	52	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( k + 1 ) = n )
54	50, 53	breqtrd 4427	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 < n )
55	46, 54	gtned 9770	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> n =/= 1 )
56	55	neneqd 2629	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. n = 1 )
57		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( k + 1 ) -> ( n - 1 ) = ( ( k + 1 ) - 1 ) )
58	57	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) = ( ( k + 1 ) - 1 ) )
59	41	nncnd 10625	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> k e. CC )
60		1cnd 9659	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> 1 e. CC )
61	59, 60	pncand 9987	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. A ) -> ( ( k + 1 ) - 1 ) = k )
62	61	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( ( k + 1 ) - 1 ) = k )
63	58, 62	eqtrd 2485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) = k )
64		simplr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> k e. A )
65	63, 64	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) e. A )
66		notnot 293	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n - 1 ) e. A <-> -. -. ( n - 1 ) e. A )
67	65, 66	sylib 200	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. -. ( n - 1 ) e. A )
68	56, 67	jca 535	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( -. n = 1 /\ -. -. ( n - 1 ) e. A ) )
69		ioran 493	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) <-> ( -. n = 1 /\ -. -. ( n - 1 ) e. A ) )
70	68, 69	sylibr 216	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. ( n = 1 \/ -. ( n - 1 ) e. A ) )
71	70	iffalsed 3892	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
72	63	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( G ` ( n - 1 ) ) = ( G ` k ) )
73	71, 72	eqtrd 2485	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` k ) )
74	14	ffvelrnda 6022	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> ( G ` k ) e. X )
75	45, 73, 43, 74	fvmptd 5954	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> ( F ` ( k + 1 ) ) = ( G ` k ) )
76	75	3adant3 1028	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( F ` ( k + 1 ) ) = ( G ` k ) )
77		simp3 1010	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( G ` k ) = y )
78	76, 77	eqtrd 2485	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( F ` ( k + 1 ) ) = y )
79		fveq2 5865	. . . . . . . . . . . . . . 15 |- ( m = ( k + 1 ) -> ( F ` m ) = ( F ` ( k + 1 ) ) )
80	79	eqeq1d 2453	. . . . . . . . . . . . . 14 |- ( m = ( k + 1 ) -> ( ( F ` m ) = y <-> ( F ` ( k + 1 ) ) = y ) )
81	80	rspcev 3150	. . . . . . . . . . . . 13 |- ( ( ( k + 1 ) e. NN /\ ( F ` ( k + 1 ) ) = y ) -> E. m e. NN ( F ` m ) = y )
82	44, 78, 81	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> E. m e. NN ( F ` m ) = y )
83	82	3exp 1207	. . . . . . . . . . 11 |- ( ph -> ( k e. A -> ( ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) ) )
84	83	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> ( k e. A -> ( ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) ) )
85	84	rexlimdv 2877	. . . . . . . . 9 |- ( ( ph /\ y e. X ) -> ( E. k e. A ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) )
86	39, 85	mpd 15	. . . . . . . 8 |- ( ( ph /\ y e. X ) -> E. m e. NN ( F ` m ) = y )
87		id 22	. . . . . . . . . . 11 |- ( ( F ` m ) = y -> ( F ` m ) = y )
88	87	eqcomd 2457	. . . . . . . . . 10 |- ( ( F ` m ) = y -> y = ( F ` m ) )
89	88	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ y e. X ) /\ m e. NN ) -> ( ( F ` m ) = y -> y = ( F ` m ) ) )
90	89	reximdva 2862	. . . . . . . 8 |- ( ( ph /\ y e. X ) -> ( E. m e. NN ( F ` m ) = y -> E. m e. NN y = ( F ` m ) ) )
91	86, 90	mpd 15	. . . . . . 7 |- ( ( ph /\ y e. X ) -> E. m e. NN y = ( F ` m ) )
92	91	adantlr 721	. . . . . 6 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ y e. X ) -> E. m e. NN y = ( F ` m ) )
93		simpll 760	. . . . . . 7 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> ph )
94		elunnel1 3575	. . . . . . . . 9 |- ( ( y e. ( X u. { (/) } ) /\ -. y e. X ) -> y e. { (/) } )
95		elsni 3993	. . . . . . . . 9 |- ( y e. { (/) } -> y = (/) )
96	94, 95	syl 17	. . . . . . . 8 |- ( ( y e. ( X u. { (/) } ) /\ -. y e. X ) -> y = (/) )
97	96	adantll 720	. . . . . . 7 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> y = (/) )
98		1nn 10620	. . . . . . . . 9 |- 1 e. NN
99	98	a1i 11	. . . . . . . 8 |- ( ( ph /\ y = (/) ) -> 1 e. NN )
100	26	a1i 11	. . . . . . . . . . 11 |- ( ph -> F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) )
101	1	orcs 396	. . . . . . . . . . . 12 |- ( n = 1 -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
102	101	adantl 468	. . . . . . . . . . 11 |- ( ( ph /\ n = 1 ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
103	98	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 e. NN )
104	3	a1i 11	. . . . . . . . . . 11 |- ( ph -> (/) e. _V )
105	100, 102, 103, 104	fvmptd 5954	. . . . . . . . . 10 |- ( ph -> ( F ` 1 ) = (/) )
106	105	adantr 467	. . . . . . . . 9 |- ( ( ph /\ y = (/) ) -> ( F ` 1 ) = (/) )
107		id 22	. . . . . . . . . . 11 |- ( y = (/) -> y = (/) )
108	107	eqcomd 2457	. . . . . . . . . 10 |- ( y = (/) -> (/) = y )
109	108	adantl 468	. . . . . . . . 9 |- ( ( ph /\ y = (/) ) -> (/) = y )
110	106, 109	eqtr2d 2486	. . . . . . . 8 |- ( ( ph /\ y = (/) ) -> y = ( F ` 1 ) )
111		fveq2 5865	. . . . . . . . . 10 |- ( m = 1 -> ( F ` m ) = ( F ` 1 ) )
112	111	eqeq2d 2461	. . . . . . . . 9 |- ( m = 1 -> ( y = ( F ` m ) <-> y = ( F ` 1 ) ) )
113	112	rspcev 3150	. . . . . . . 8 |- ( ( 1 e. NN /\ y = ( F ` 1 ) ) -> E. m e. NN y = ( F ` m ) )
114	99, 110, 113	syl2anc 667	. . . . . . 7 |- ( ( ph /\ y = (/) ) -> E. m e. NN y = ( F ` m ) )
115	93, 97, 114	syl2anc 667	. . . . . 6 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> E. m e. NN y = ( F ` m ) )
116	92, 115	pm2.61dan 800	. . . . 5 |- ( ( ph /\ y e. ( X u. { (/) } ) ) -> E. m e. NN y = ( F ` m ) )
117	116	ralrimiva 2802	. . . 4 |- ( ph -> A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) )
118	27, 117	jca 535	. . 3 |- ( ph -> ( F : NN --> ( X u. { (/) } ) /\ A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) ) )
119		dffo3 6037	. . 3 |- ( F : NN -onto-> ( X u. { (/) } ) <-> ( F : NN --> ( X u. { (/) } ) /\ A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) ) )
120	118, 119	sylibr 216	. 2 |- ( ph -> F : NN -onto-> ( X u. { (/) } ) )
121		orc 387	. . . . . 6 |- ( n = m -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
122	121	adantl 468	. . . . 5 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n = m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
123		simpl 459	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> ( ph /\ ( n e. NN /\ m e. NN ) ) )
124		neqne 37374	. . . . . . 7 |- ( -. n = m -> n =/= m )
125	124	adantl 468	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> n =/= m )
126		simpl 459	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> n e. NN )
127	2, 3	syl6eqel 2537	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V )
128	26	fvmpt2 5957	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V ) -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
129	126, 127, 128	syl2anc 667	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
130	129, 2	eqtrd 2485	. . . . . . . . . . . 12 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = (/) )
131	130	ineq1d 3633	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( (/) i^i ( F ` m ) ) )
132		0in 37393	. . . . . . . . . . . 12 |- ( (/) i^i ( F ` m ) ) = (/)
133	132	a1i 11	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( (/) i^i ( F ` m ) ) = (/) )
134	131, 133	eqtrd 2485	. . . . . . . . . 10 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
135	134	adantlr 721	. . . . . . . . 9 |- ( ( ( n e. NN /\ m e. NN ) /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
136	135	ad4ant24 1240	. . . . . . . 8 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
137	26	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) )
138		eqeq1 2455	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( n = 1 <-> m = 1 ) )
139		oveq1 6297	. . . . . . . . . . . . . . . . . . . 20 |- ( n = m -> ( n - 1 ) = ( m - 1 ) )
140	139	eleq1d 2513	. . . . . . . . . . . . . . . . . . 19 |- ( n = m -> ( ( n - 1 ) e. A <-> ( m - 1 ) e. A ) )
141	140	notbid 296	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( -. ( n - 1 ) e. A <-> -. ( m - 1 ) e. A ) )
142	138, 141	orbi12d 716	. . . . . . . . . . . . . . . . 17 |- ( n = m -> ( ( n = 1 \/ -. ( n - 1 ) e. A ) <-> ( m = 1 \/ -. ( m - 1 ) e. A ) ) )
143		eqidd 2452	. . . . . . . . . . . . . . . . 17 |- ( n = m -> (/) = (/) )
144	139	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( n = m -> ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) )
145	142, 143, 144	ifbieq12d 3908	. . . . . . . . . . . . . . . 16 |- ( n = m -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
146	145	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) /\ n = m ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
147		simpl 459	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> m e. NN )
148		iftrue 3887	. . . . . . . . . . . . . . . . 17 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = (/) )
149	3	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> (/) e. _V )
150	148, 149	eqeltrd 2529	. . . . . . . . . . . . . . . 16 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) e. _V )
151	150	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) e. _V )
152	137, 146, 147, 151	fvmptd 5954	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
153	148	adantl 468	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = (/) )
154	152, 153	eqtrd 2485	. . . . . . . . . . . . 13 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = (/) )
155	154	ineq2d 3634	. . . . . . . . . . . 12 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( ( F ` n ) i^i (/) ) )
156		in0 3760	. . . . . . . . . . . . 13 |- ( ( F ` n ) i^i (/) ) = (/)
157	156	a1i 11	. . . . . . . . . . . 12 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i (/) ) = (/) )
158	155, 157	eqtrd 2485	. . . . . . . . . . 11 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
159	158	adantll 720	. . . . . . . . . 10 |- ( ( ( n e. NN /\ m e. NN ) /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
160	159	ad5ant25 1248	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
161		id 22	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> n e. NN )
162		fvex 5875	. . . . . . . . . . . . . . . . . . 19 |- ( G ` ( n - 1 ) ) e. _V
163	3, 162	ifex 3949	. . . . . . . . . . . . . . . . . 18 |- if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V
164	163	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V )
165	161, 164, 128	syl2anc 667	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
166	165	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
167	10	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
168	166, 167	eqtrd 2485	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
169	168	adantlr 721	. . . . . . . . . . . . 13 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
170	169	3adant3 1028	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
171	26	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) )
172	145	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) /\ n = m ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
173		iffalse 3890	. . . . . . . . . . . . . . . . 17 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = ( G ` ( m - 1 ) ) )
174	173	ad2antlr 733	. . . . . . . . . . . . . . . 16 |- ( ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) /\ n = m ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = ( G ` ( m - 1 ) ) )
175	172, 174	eqtrd 2485	. . . . . . . . . . . . . . 15 |- ( ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) /\ n = m ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( m - 1 ) ) )
176		simpl 459	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> m e. NN )
177		fvex 5875	. . . . . . . . . . . . . . . 16 |- ( G ` ( m - 1 ) ) e. _V
178	177	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( m - 1 ) ) e. _V )
179	171, 175, 176, 178	fvmptd 5954	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
180	179	adantll 720	. . . . . . . . . . . . 13 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
181	180	3adant2 1027	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
182	170, 181	ineq12d 3635	. . . . . . . . . . 11 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) )
183	182	ad5ant245 1249	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) )
184	18	ad2antlr 733	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( n - 1 ) e. A )
185		pm2.46 400	. . . . . . . . . . . . . . . 16 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> -. -. ( m - 1 ) e. A )
186	185	notnotrd 117	. . . . . . . . . . . . . . 15 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> ( m - 1 ) e. A )
187	186	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( m - 1 ) e. A )
188		f1of1 5813	. . . . . . . . . . . . . . . . . . 19 |- ( G : A -1-1-onto-> X -> G : A -1-1-> X )
189	12, 188	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : A -1-1-> X )
190		dff14a 6170	. . . . . . . . . . . . . . . . . 18 |- ( G : A -1-1-> X <-> ( G : A --> X /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) )
191	189, 190	sylib 200	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G : A --> X /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) )
192	191	simprd 465	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) )
193	192	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. NN /\ m e. NN ) ) -> A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) )
194	193	ad3antrrr 736	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) )
195	184, 187, 194	jca31 537	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( ( n - 1 ) e. A /\ ( m - 1 ) e. A ) /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) )
196		nncn 10617	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> n e. CC )
197	196	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN /\ m e. NN ) -> n e. CC )
198	197	ad2antlr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> n e. CC )
199		nncn 10617	. . . . . . . . . . . . . . . . 17 |- ( m e. NN -> m e. CC )
200	199	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN /\ m e. NN ) -> m e. CC )
201	200	ad2antlr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> m e. CC )
202		1cnd 9659	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> 1 e. CC )
203		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> n =/= m )
204	198, 201, 202, 203	subneintr2d 10032	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( n - 1 ) =/= ( m - 1 ) )
205	204	ad2antrr 732	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( n - 1 ) =/= ( m - 1 ) )
206		neeq1 2686	. . . . . . . . . . . . . . 15 |- ( x = ( n - 1 ) -> ( x =/= y <-> ( n - 1 ) =/= y ) )
207		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( x = ( n - 1 ) -> ( G ` x ) = ( G ` ( n - 1 ) ) )
208	207	neeq1d 2683	. . . . . . . . . . . . . . 15 |- ( x = ( n - 1 ) -> ( ( G ` x ) =/= ( G ` y ) <-> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) )
209	206, 208	imbi12d 322	. . . . . . . . . . . . . 14 |- ( x = ( n - 1 ) -> ( ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) <-> ( ( n - 1 ) =/= y -> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) ) )
210		neeq2 2687	. . . . . . . . . . . . . . 15 |- ( y = ( m - 1 ) -> ( ( n - 1 ) =/= y <-> ( n - 1 ) =/= ( m - 1 ) ) )
211		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( y = ( m - 1 ) -> ( G ` y ) = ( G ` ( m - 1 ) ) )
212	211	neeq2d 2684	. . . . . . . . . . . . . . 15 |- ( y = ( m - 1 ) -> ( ( G ` ( n - 1 ) ) =/= ( G ` y ) <-> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) ) )
213	210, 212	imbi12d 322	. . . . . . . . . . . . . 14 |- ( y = ( m - 1 ) -> ( ( ( n - 1 ) =/= y -> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) <-> ( ( n - 1 ) =/= ( m - 1 ) -> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) ) ) )
214	209, 213	rspc2va 3160	. . . . . . . . . . . . 13 |- ( ( ( ( n - 1 ) e. A /\ ( m - 1 ) e. A ) /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) -> ( ( n - 1 ) =/= ( m - 1 ) -> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) ) )
215	195, 205, 214	sylc 62	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) )
216	215	neneqd 2629	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> -. ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) )
217	20	ad4ant13 1234	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. X )
218		simpl 459	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ph )
219	186	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( m - 1 ) e. A )
220	14	ffvelrnda 6022	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( m - 1 ) e. A ) -> ( G ` ( m - 1 ) ) e. X )
221	218, 219, 220	syl2anc 667	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( m - 1 ) ) e. X )
222	221	ad4ant14 1235	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( m - 1 ) ) e. X )
223		nnfoctbdjlem.dj	. . . . . . . . . . . . . . 15 |- ( ph -> Disj y e. X y )
224		id 22	. . . . . . . . . . . . . . . 16 |- ( y = z -> y = z )
225	224	disjor 4387	. . . . . . . . . . . . . . 15 |- (Disj y e. X y <-> A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) )
226	223, 225	sylib 200	. . . . . . . . . . . . . 14 |- ( ph -> A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) )
227	226	ad3antrrr 736	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) )
228		eqeq1 2455	. . . . . . . . . . . . . . 15 |- ( y = ( G ` ( n - 1 ) ) -> ( y = z <-> ( G ` ( n - 1 ) ) = z ) )
229		ineq1 3627	. . . . . . . . . . . . . . . 16 |- ( y = ( G ` ( n - 1 ) ) -> ( y i^i z ) = ( ( G ` ( n - 1 ) ) i^i z ) )
230	229	eqeq1d 2453	. . . . . . . . . . . . . . 15 |- ( y = ( G ` ( n - 1 ) ) -> ( ( y i^i z ) = (/) <-> ( ( G ` ( n - 1 ) ) i^i z ) = (/) ) )
231	228, 230	orbi12d 716	. . . . . . . . . . . . . 14 |- ( y = ( G ` ( n - 1 ) ) -> ( ( y = z \/ ( y i^i z ) = (/) ) <-> ( ( G ` ( n - 1 ) ) = z \/ ( ( G ` ( n - 1 ) ) i^i z ) = (/) ) ) )
232		eqeq2 2462	. . . . . . . . . . . . . . 15 |- ( z = ( G ` ( m - 1 ) ) -> ( ( G ` ( n - 1 ) ) = z <-> ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) ) )
233		ineq2 3628	. . . . . . . . . . . . . . . 16 |- ( z = ( G ` ( m - 1 ) ) -> ( ( G ` ( n - 1 ) ) i^i z ) = ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) )
234	233	eqeq1d 2453	. . . . . . . . . . . . . . 15 |- ( z = ( G ` ( m - 1 ) ) -> ( ( ( G ` ( n - 1 ) ) i^i z ) = (/) <-> ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
235	232, 234	orbi12d 716	. . . . . . . . . . . . . 14 |- ( z = ( G ` ( m - 1 ) ) -> ( ( ( G ` ( n - 1 ) ) = z \/ ( ( G ` ( n - 1 ) ) i^i z ) = (/) ) <-> ( ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) \/ ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) ) )
236	231, 235	rspc2va 3160	. . . . . . . . . . . . 13 |- ( ( ( ( G ` ( n - 1 ) ) e. X /\ ( G ` ( m - 1 ) ) e. X ) /\ A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) ) -> ( ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) \/ ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
237	217, 222, 227, 236	syl21anc 1267	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) \/ ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
238	237	adantllr 725	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) \/ ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
239		orel1 384	. . . . . . . . . . 11 |- ( -. ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) -> ( ( ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) \/ ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) -> ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
240	216, 238, 239	sylc 62	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) )
241	183, 240	eqtrd 2485	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
242	160, 241	pm2.61dan 800	. . . . . . . 8 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
243	136, 242	pm2.61dan 800	. . . . . . 7 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
244		olc 386	. . . . . . 7 |- ( ( ( F ` n ) i^i ( F ` m ) ) = (/) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
245	243, 244	syl 17	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
246	123, 125, 245	syl2anc 667	. . . . 5 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
247	122, 246	pm2.61dan 800	. . . 4 |- ( ( ph /\ ( n e. NN /\ m e. NN ) ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
248	247	ralrimivva 2809	. . 3 |- ( ph -> A. n e. NN A. m e. NN ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
249		fveq2 5865	. . . 4 |- ( n = m -> ( F ` n ) = ( F ` m ) )
250	249	disjor 4387	. . 3 |- (Disj n e. NN ( F ` n ) <-> A. n e. NN A. m e. NN ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
251	248, 250	sylibr 216	. 2 |- ( ph -> Disj n e. NN ( F ` n ) )
252		nnex 10615	. . . . 5 |- NN e. _V
253	252	mptex 6136	. . . 4 |- ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) e. _V
254	26, 253	eqeltri 2525	. . 3 |- F e. _V
255		foeq1 5789	. . . 4 |- ( f = F -> ( f : NN -onto-> ( X u. { (/) } ) <-> F : NN -onto-> ( X u. { (/) } ) ) )
256		simpl 459	. . . . . 6 |- ( ( f = F /\ n e. NN ) -> f = F )
257	256	fveq1d 5867	. . . . 5 |- ( ( f = F /\ n e. NN ) -> ( f ` n ) = ( F ` n ) )
258	257	disjeq2dv 4378	. . . 4 |- ( f = F -> (Disj n e. NN ( f ` n ) <-> Disj n e. NN ( F ` n ) ) )
259	255, 258	anbi12d 717	. . 3 |- ( f = F -> ( ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) <-> ( F : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( F ` n ) ) ) )
260	254, 259	spcev 3141	. 2 |- ( ( F : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( F ` n ) ) -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )
261	120, 251, 260	syl2anc 667	1 |- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 985   = wceq 1444   E.wex 1663   e. wcel 1887   =/= wne 2622   A.wral 2737   E.wrex 2738   _Vcvv 3045   u. cun 3402   i^i cin 3403   C_ wss 3404   (/)c0 3731   ifcif 3881   {csn 3968  Disj wdisj 4373   class class class wbr 4402   |-> cmpt 4461   ran crn 4835   Fn wfn 5577   -->wf 5578   -1-1->wf1 5579   -onto->wfo 5580   -1-1-onto->wf1o 5581   ` cfv 5582  (class class class)co 6290   CCcc 9537   1c1 9540   + caddc 9542   < clt 9675   - cmin 9860   NNcn 10609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-rp 11303

This theorem is referenced by:  nnfoctbdj  38294