Theorem nnfoctbdjlem 38409

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 3878	. . . . . . . . 9 |- ( ( n = 1 \/ -. ( n - 1 ) e. A ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
2	1	adantl 473	. . . . . . . 8 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
3		0ex 4528	. . . . . . . . . . 11 |- (/) e. _V
4	3	snid 3988	. . . . . . . . . 10 |- (/) e. { (/) }
5		elun2 3593	. . . . . . . . . 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 2549	. . . . . . 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 728	. . . . . 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 3881	. . . . . . . 8 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
11	10	adantl 473	. . . . . . 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 5828	. . . . . . . . . . . 12 |- ( G : A -1-1-onto-> X -> G : A --> X )
14	12, 13	syl 17	. . . . . . . . . . 11 |- ( ph -> G : A --> X )
15	14	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> G : A --> X )
16		pm2.46 405	. . . . . . . . . . . 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 473	. . . . . . . . . 10 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( n - 1 ) e. A )
20	15, 19	ffvelrnd 6038	. . . . . . . . 9 |- ( ( ph /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. X )
21	20	adantlr 729	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( G ` ( n - 1 ) ) e. X )
22		elun1 3592	. . . . . . . 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 2549	. . . . . 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 808	. . . . 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 6061	. . . 4 |- ( ph -> F : NN --> ( X u. { (/) } ) )
28		simpr 468	. . . . . . . . . . 11 |- ( ( ph /\ y e. X ) -> y e. X )
29		f1ofo 5835	. . . . . . . . . . . . . 14 |- ( G : A -1-1-onto-> X -> G : A -onto-> X )
30		forn 5809	. . . . . . . . . . . . . 14 |- ( G : A -onto-> X -> ran G = X )
31	12, 29, 30	3syl 18	. . . . . . . . . . . . 13 |- ( ph -> ran G = X )
32	31	eqcomd 2477	. . . . . . . . . . . 12 |- ( ph -> X = ran G )
33	32	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ y e. X ) -> X = ran G )
34	28, 33	eleqtrd 2551	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> y e. ran G )
35	14	ffnd 5740	. . . . . . . . . . . 12 |- ( ph -> G Fn A )
36		fvelrnb 5926	. . . . . . . . . . . 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 472	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> ( y e. ran G <-> E. k e. A ( G ` k ) = y ) )
39	34, 38	mpbid 215	. . . . . . . . 9 |- ( ( ph /\ y e. X ) -> E. k e. A ( G ` k ) = y )
40		nnfoctbdjlem.a	. . . . . . . . . . . . . . . 16 |- ( ph -> A C_ NN )
41	40	sselda 3418	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> k e. NN )
42		peano2nn 10643	. . . . . . . . . . . . . . 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 1050	. . . . . . . . . . . . 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 9676	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 e. RR )
47		1red 9676	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> 1 e. RR )
48	41	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> k e. RR+ )
49	47, 48	ltaddrp2d 11395	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. A ) -> 1 < ( k + 1 ) )
50	49	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 < ( k + 1 ) )
51		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = ( k + 1 ) -> n = ( k + 1 ) )
52	51	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( k + 1 ) -> ( k + 1 ) = n )
53	52	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( k + 1 ) = n )
54	50, 53	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> 1 < n )
55	46, 54	gtned 9787	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> n =/= 1 )
56	55	neneqd 2648	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. n = 1 )
57		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = ( k + 1 ) -> ( n - 1 ) = ( ( k + 1 ) - 1 ) )
58	57	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) = ( ( k + 1 ) - 1 ) )
59	41	nncnd 10647	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> k e. CC )
60		1cnd 9677	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. A ) -> 1 e. CC )
61	59, 60	pncand 10006	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. A ) -> ( ( k + 1 ) - 1 ) = k )
62	61	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( ( k + 1 ) - 1 ) = k )
63	58, 62	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) = k )
64		simplr 770	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> k e. A )
65	63, 64	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( n - 1 ) e. A )
66	65	notnotd 128	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. -. ( n - 1 ) e. A )
67	56, 66	jca 541	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( -. n = 1 /\ -. -. ( n - 1 ) e. A ) )
68		ioran 498	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( n = 1 \/ -. ( n - 1 ) e. A ) <-> ( -. n = 1 /\ -. -. ( n - 1 ) e. A ) )
69	67, 68	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> -. ( n = 1 \/ -. ( n - 1 ) e. A ) )
70	69	iffalsed 3883	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
71	63	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> ( G ` ( n - 1 ) ) = ( G ` k ) )
72	70, 71	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. A ) /\ n = ( k + 1 ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` k ) )
73	14	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. A ) -> ( G ` k ) e. X )
74	45, 72, 43, 73	fvmptd 5969	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> ( F ` ( k + 1 ) ) = ( G ` k ) )
75	74	3adant3 1050	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( F ` ( k + 1 ) ) = ( G ` k ) )
76		simp3 1032	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( G ` k ) = y )
77	75, 76	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> ( F ` ( k + 1 ) ) = y )
78		fveq2 5879	. . . . . . . . . . . . . . 15 |- ( m = ( k + 1 ) -> ( F ` m ) = ( F ` ( k + 1 ) ) )
79	78	eqeq1d 2473	. . . . . . . . . . . . . 14 |- ( m = ( k + 1 ) -> ( ( F ` m ) = y <-> ( F ` ( k + 1 ) ) = y ) )
80	79	rspcev 3136	. . . . . . . . . . . . 13 |- ( ( ( k + 1 ) e. NN /\ ( F ` ( k + 1 ) ) = y ) -> E. m e. NN ( F ` m ) = y )
81	44, 77, 80	syl2anc 673	. . . . . . . . . . . 12 |- ( ( ph /\ k e. A /\ ( G ` k ) = y ) -> E. m e. NN ( F ` m ) = y )
82	81	3exp 1230	. . . . . . . . . . 11 |- ( ph -> ( k e. A -> ( ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) ) )
83	82	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ y e. X ) -> ( k e. A -> ( ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) ) )
84	83	rexlimdv 2870	. . . . . . . . 9 |- ( ( ph /\ y e. X ) -> ( E. k e. A ( G ` k ) = y -> E. m e. NN ( F ` m ) = y ) )
85	39, 84	mpd 15	. . . . . . . 8 |- ( ( ph /\ y e. X ) -> E. m e. NN ( F ` m ) = y )
86		id 22	. . . . . . . . . . 11 |- ( ( F ` m ) = y -> ( F ` m ) = y )
87	86	eqcomd 2477	. . . . . . . . . 10 |- ( ( F ` m ) = y -> y = ( F ` m ) )
88	87	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ y e. X ) /\ m e. NN ) -> ( ( F ` m ) = y -> y = ( F ` m ) ) )
89	88	reximdva 2858	. . . . . . . 8 |- ( ( ph /\ y e. X ) -> ( E. m e. NN ( F ` m ) = y -> E. m e. NN y = ( F ` m ) ) )
90	85, 89	mpd 15	. . . . . . 7 |- ( ( ph /\ y e. X ) -> E. m e. NN y = ( F ` m ) )
91	90	adantlr 729	. . . . . 6 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ y e. X ) -> E. m e. NN y = ( F ` m ) )
92		simpll 768	. . . . . . 7 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> ph )
93		elunnel1 3566	. . . . . . . . 9 |- ( ( y e. ( X u. { (/) } ) /\ -. y e. X ) -> y e. { (/) } )
94		elsni 3985	. . . . . . . . 9 |- ( y e. { (/) } -> y = (/) )
95	93, 94	syl 17	. . . . . . . 8 |- ( ( y e. ( X u. { (/) } ) /\ -. y e. X ) -> y = (/) )
96	95	adantll 728	. . . . . . 7 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> y = (/) )
97		1nn 10642	. . . . . . . . 9 |- 1 e. NN
98	97	a1i 11	. . . . . . . 8 |- ( ( ph /\ y = (/) ) -> 1 e. NN )
99	26	a1i 11	. . . . . . . . . . 11 |- ( ph -> F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) )
100	1	orcs 401	. . . . . . . . . . . 12 |- ( n = 1 -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
101	100	adantl 473	. . . . . . . . . . 11 |- ( ( ph /\ n = 1 ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = (/) )
102	97	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 e. NN )
103	3	a1i 11	. . . . . . . . . . 11 |- ( ph -> (/) e. _V )
104	99, 101, 102, 103	fvmptd 5969	. . . . . . . . . 10 |- ( ph -> ( F ` 1 ) = (/) )
105	104	adantr 472	. . . . . . . . 9 |- ( ( ph /\ y = (/) ) -> ( F ` 1 ) = (/) )
106		id 22	. . . . . . . . . . 11 |- ( y = (/) -> y = (/) )
107	106	eqcomd 2477	. . . . . . . . . 10 |- ( y = (/) -> (/) = y )
108	107	adantl 473	. . . . . . . . 9 |- ( ( ph /\ y = (/) ) -> (/) = y )
109	105, 108	eqtr2d 2506	. . . . . . . 8 |- ( ( ph /\ y = (/) ) -> y = ( F ` 1 ) )
110		fveq2 5879	. . . . . . . . . 10 |- ( m = 1 -> ( F ` m ) = ( F ` 1 ) )
111	110	eqeq2d 2481	. . . . . . . . 9 |- ( m = 1 -> ( y = ( F ` m ) <-> y = ( F ` 1 ) ) )
112	111	rspcev 3136	. . . . . . . 8 |- ( ( 1 e. NN /\ y = ( F ` 1 ) ) -> E. m e. NN y = ( F ` m ) )
113	98, 109, 112	syl2anc 673	. . . . . . 7 |- ( ( ph /\ y = (/) ) -> E. m e. NN y = ( F ` m ) )
114	92, 96, 113	syl2anc 673	. . . . . 6 |- ( ( ( ph /\ y e. ( X u. { (/) } ) ) /\ -. y e. X ) -> E. m e. NN y = ( F ` m ) )
115	91, 114	pm2.61dan 808	. . . . 5 |- ( ( ph /\ y e. ( X u. { (/) } ) ) -> E. m e. NN y = ( F ` m ) )
116	115	ralrimiva 2809	. . . 4 |- ( ph -> A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) )
117	27, 116	jca 541	. . 3 |- ( ph -> ( F : NN --> ( X u. { (/) } ) /\ A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) ) )
118		dffo3 6052	. . 3 |- ( F : NN -onto-> ( X u. { (/) } ) <-> ( F : NN --> ( X u. { (/) } ) /\ A. y e. ( X u. { (/) } ) E. m e. NN y = ( F ` m ) ) )
119	117, 118	sylibr 217	. 2 |- ( ph -> F : NN -onto-> ( X u. { (/) } ) )
120		orc 392	. . . . . 6 |- ( n = m -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
121	120	adantl 473	. . . . 5 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n = m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
122		simpl 464	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> ( ph /\ ( n e. NN /\ m e. NN ) ) )
123		neqne 2651	. . . . . . 7 |- ( -. n = m -> n =/= m )
124	123	adantl 473	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> n =/= m )
125		simpl 464	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> n e. NN )
126	2, 3	syl6eqel 2557	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V )
127	26	fvmpt2 5972	. . . . . . . . . . . . . 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 ) ) ) )
128	125, 126, 127	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
129	128, 2	eqtrd 2505	. . . . . . . . . . . 12 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = (/) )
130	129	ineq1d 3624	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( (/) i^i ( F ` m ) ) )
131		0in 37452	. . . . . . . . . . . 12 |- ( (/) i^i ( F ` m ) ) = (/)
132	131	a1i 11	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( (/) i^i ( F ` m ) ) = (/) )
133	130, 132	eqtrd 2505	. . . . . . . . . 10 |- ( ( n e. NN /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
134	133	adantlr 729	. . . . . . . . 9 |- ( ( ( n e. NN /\ m e. NN ) /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
135	134	ad4ant24 1264	. . . . . . . 8 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
136	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 ) ) ) ) )
137		eqeq1 2475	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( n = 1 <-> m = 1 ) )
138		oveq1 6315	. . . . . . . . . . . . . . . . . . . 20 |- ( n = m -> ( n - 1 ) = ( m - 1 ) )
139	138	eleq1d 2533	. . . . . . . . . . . . . . . . . . 19 |- ( n = m -> ( ( n - 1 ) e. A <-> ( m - 1 ) e. A ) )
140	139	notbid 301	. . . . . . . . . . . . . . . . . 18 |- ( n = m -> ( -. ( n - 1 ) e. A <-> -. ( m - 1 ) e. A ) )
141	137, 140	orbi12d 724	. . . . . . . . . . . . . . . . 17 |- ( n = m -> ( ( n = 1 \/ -. ( n - 1 ) e. A ) <-> ( m = 1 \/ -. ( m - 1 ) e. A ) ) )
142		eqidd 2472	. . . . . . . . . . . . . . . . 17 |- ( n = m -> (/) = (/) )
143	138	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( n = m -> ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) )
144	141, 142, 143	ifbieq12d 3899	. . . . . . . . . . . . . . . 16 |- ( n = m -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
145	144	adantl 473	. . . . . . . . . . . . . . 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 ) ) ) )
146		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> m e. NN )
147		iftrue 3878	. . . . . . . . . . . . . . . . 17 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = (/) )
148	3	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> (/) e. _V )
149	147, 148	eqeltrd 2549	. . . . . . . . . . . . . . . 16 |- ( ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) e. _V )
150	149	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) e. _V )
151	136, 145, 146, 150	fvmptd 5969	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) )
152	147	adantl 473	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = (/) )
153	151, 152	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = (/) )
154	153	ineq2d 3625	. . . . . . . . . . . 12 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = ( ( F ` n ) i^i (/) ) )
155		in0 3763	. . . . . . . . . . . . 13 |- ( ( F ` n ) i^i (/) ) = (/)
156	155	a1i 11	. . . . . . . . . . . 12 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i (/) ) = (/) )
157	154, 156	eqtrd 2505	. . . . . . . . . . 11 |- ( ( m e. NN /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
158	157	adantll 728	. . . . . . . . . 10 |- ( ( ( n e. NN /\ m e. NN ) /\ ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
159	158	ad5ant25 1272	. . . . . . . . 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 ) ) = (/) )
160		id 22	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> n e. NN )
161		fvex 5889	. . . . . . . . . . . . . . . . . . 19 |- ( G ` ( n - 1 ) ) e. _V
162	3, 161	ifex 3940	. . . . . . . . . . . . . . . . . 18 |- if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V
163	162	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) e. _V )
164	160, 163, 127	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
165	164	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
166	10	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) = ( G ` ( n - 1 ) ) )
167	165, 166	eqtrd 2505	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
168	167	adantlr 729	. . . . . . . . . . . . 13 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
169	168	3adant3 1050	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` n ) = ( G ` ( n - 1 ) ) )
170	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 ) ) ) ) )
171	144	adantl 473	. . . . . . . . . . . . . . . 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 ) ) ) )
172		iffalse 3881	. . . . . . . . . . . . . . . . 17 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> if ( ( m = 1 \/ -. ( m - 1 ) e. A ) , (/) , ( G ` ( m - 1 ) ) ) = ( G ` ( m - 1 ) ) )
173	172	ad2antlr 741	. . . . . . . . . . . . . . . 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 ) ) )
174	171, 173	eqtrd 2505	. . . . . . . . . . . . . . 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 ) ) )
175		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> m e. NN )
176		fvex 5889	. . . . . . . . . . . . . . . 16 |- ( G ` ( m - 1 ) ) e. _V
177	176	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( m - 1 ) ) e. _V )
178	170, 174, 175, 177	fvmptd 5969	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
179	178	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
180	179	3adant2 1049	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ m e. NN ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( F ` m ) = ( G ` ( m - 1 ) ) )
181	169, 180	ineq12d 3626	. . . . . . . . . . 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 ) ) ) )
182	181	ad5ant245 1273	. . . . . . . . . 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 ) ) ) )
183	18	ad2antlr 741	. . . . . . . . . . . . . 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 )
184		pm2.46 405	. . . . . . . . . . . . . . . 16 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> -. -. ( m - 1 ) e. A )
185	184	notnotrd 117	. . . . . . . . . . . . . . 15 |- ( -. ( m = 1 \/ -. ( m - 1 ) e. A ) -> ( m - 1 ) e. A )
186	185	adantl 473	. . . . . . . . . . . . . 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 )
187		f1of1 5827	. . . . . . . . . . . . . . . . . . 19 |- ( G : A -1-1-onto-> X -> G : A -1-1-> X )
188	12, 187	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : A -1-1-> X )
189		dff14a 6188	. . . . . . . . . . . . . . . . . 18 |- ( G : A -1-1-> X <-> ( G : A --> X /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) )
190	188, 189	sylib 201	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G : A --> X /\ A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) ) )
191	190	simprd 470	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) )
192	191	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. NN /\ m e. NN ) ) -> A. x e. A A. y e. A ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) )
193	192	ad3antrrr 744	. . . . . . . . . . . . . 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 ) ) )
194	183, 186, 193	jca31 543	. . . . . . . . . . . . 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 ) ) ) )
195		nncn 10639	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> n e. CC )
196	195	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN /\ m e. NN ) -> n e. CC )
197	196	ad2antlr 741	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> n e. CC )
198		nncn 10639	. . . . . . . . . . . . . . . . 17 |- ( m e. NN -> m e. CC )
199	198	adantl 473	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN /\ m e. NN ) -> m e. CC )
200	199	ad2antlr 741	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> m e. CC )
201		1cnd 9677	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> 1 e. CC )
202		simpr 468	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> n =/= m )
203	197, 200, 201, 202	subneintr2d 10051	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( n - 1 ) =/= ( m - 1 ) )
204	203	ad2antrr 740	. . . . . . . . . . . . 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 ) )
205		neeq1 2705	. . . . . . . . . . . . . . 15 |- ( x = ( n - 1 ) -> ( x =/= y <-> ( n - 1 ) =/= y ) )
206		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( x = ( n - 1 ) -> ( G ` x ) = ( G ` ( n - 1 ) ) )
207	206	neeq1d 2702	. . . . . . . . . . . . . . 15 |- ( x = ( n - 1 ) -> ( ( G ` x ) =/= ( G ` y ) <-> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) )
208	205, 207	imbi12d 327	. . . . . . . . . . . . . 14 |- ( x = ( n - 1 ) -> ( ( x =/= y -> ( G ` x ) =/= ( G ` y ) ) <-> ( ( n - 1 ) =/= y -> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) ) )
209		neeq2 2706	. . . . . . . . . . . . . . 15 |- ( y = ( m - 1 ) -> ( ( n - 1 ) =/= y <-> ( n - 1 ) =/= ( m - 1 ) ) )
210		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( y = ( m - 1 ) -> ( G ` y ) = ( G ` ( m - 1 ) ) )
211	210	neeq2d 2703	. . . . . . . . . . . . . . 15 |- ( y = ( m - 1 ) -> ( ( G ` ( n - 1 ) ) =/= ( G ` y ) <-> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) ) )
212	209, 211	imbi12d 327	. . . . . . . . . . . . . 14 |- ( y = ( m - 1 ) -> ( ( ( n - 1 ) =/= y -> ( G ` ( n - 1 ) ) =/= ( G ` y ) ) <-> ( ( n - 1 ) =/= ( m - 1 ) -> ( G ` ( n - 1 ) ) =/= ( G ` ( m - 1 ) ) ) ) )
213	208, 212	rspc2va 3148	. . . . . . . . . . . . 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 ) ) ) )
214	194, 204, 213	sylc 61	. . . . . . . . . . . 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 ) ) )
215	214	neneqd 2648	. . . . . . . . . . 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 ) ) )
216	20	ad4ant13 1258	. . . . . . . . . . . . 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 )
217		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ph )
218	185	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( m - 1 ) e. A )
219	14	ffvelrnda 6037	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( m - 1 ) e. A ) -> ( G ` ( m - 1 ) ) e. X )
220	217, 218, 219	syl2anc 673	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( m = 1 \/ -. ( m - 1 ) e. A ) ) -> ( G ` ( m - 1 ) ) e. X )
221	220	ad4ant14 1259	. . . . . . . . . . . . 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 )
222		nnfoctbdjlem.dj	. . . . . . . . . . . . . . 15 |- ( ph -> Disj y e. X y )
223		id 22	. . . . . . . . . . . . . . . 16 |- ( y = z -> y = z )
224	223	disjor 4380	. . . . . . . . . . . . . . 15 |- (Disj y e. X y <-> A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) )
225	222, 224	sylib 201	. . . . . . . . . . . . . 14 |- ( ph -> A. y e. X A. z e. X ( y = z \/ ( y i^i z ) = (/) ) )
226	225	ad3antrrr 744	. . . . . . . . . . . . 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 ) = (/) ) )
227		eqeq1 2475	. . . . . . . . . . . . . . 15 |- ( y = ( G ` ( n - 1 ) ) -> ( y = z <-> ( G ` ( n - 1 ) ) = z ) )
228		ineq1 3618	. . . . . . . . . . . . . . . 16 |- ( y = ( G ` ( n - 1 ) ) -> ( y i^i z ) = ( ( G ` ( n - 1 ) ) i^i z ) )
229	228	eqeq1d 2473	. . . . . . . . . . . . . . 15 |- ( y = ( G ` ( n - 1 ) ) -> ( ( y i^i z ) = (/) <-> ( ( G ` ( n - 1 ) ) i^i z ) = (/) ) )
230	227, 229	orbi12d 724	. . . . . . . . . . . . . 14 |- ( y = ( G ` ( n - 1 ) ) -> ( ( y = z \/ ( y i^i z ) = (/) ) <-> ( ( G ` ( n - 1 ) ) = z \/ ( ( G ` ( n - 1 ) ) i^i z ) = (/) ) ) )
231		eqeq2 2482	. . . . . . . . . . . . . . 15 |- ( z = ( G ` ( m - 1 ) ) -> ( ( G ` ( n - 1 ) ) = z <-> ( G ` ( n - 1 ) ) = ( G ` ( m - 1 ) ) ) )
232		ineq2 3619	. . . . . . . . . . . . . . . 16 |- ( z = ( G ` ( m - 1 ) ) -> ( ( G ` ( n - 1 ) ) i^i z ) = ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) )
233	232	eqeq1d 2473	. . . . . . . . . . . . . . 15 |- ( z = ( G ` ( m - 1 ) ) -> ( ( ( G ` ( n - 1 ) ) i^i z ) = (/) <-> ( ( G ` ( n - 1 ) ) i^i ( G ` ( m - 1 ) ) ) = (/) ) )
234	231, 233	orbi12d 724	. . . . . . . . . . . . . 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 ) ) ) = (/) ) ) )
235	230, 234	rspc2va 3148	. . . . . . . . . . . . 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 ) ) ) = (/) ) )
236	216, 221, 226, 235	syl21anc 1291	. . . . . . . . . . . 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 ) ) ) = (/) ) )
237	236	adantllr 733	. . . . . . . . . . 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 ) ) ) = (/) ) )
238		orel1 389	. . . . . . . . . . 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 ) ) ) = (/) ) )
239	215, 237, 238	sylc 61	. . . . . . . . . 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 ) ) ) = (/) )
240	182, 239	eqtrd 2505	. . . . . . . . 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 ) ) = (/) )
241	159, 240	pm2.61dan 808	. . . . . . . 8 |- ( ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) /\ -. ( n = 1 \/ -. ( n - 1 ) e. A ) ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
242	135, 241	pm2.61dan 808	. . . . . . 7 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( ( F ` n ) i^i ( F ` m ) ) = (/) )
243		olc 391	. . . . . . 7 |- ( ( ( F ` n ) i^i ( F ` m ) ) = (/) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
244	242, 243	syl 17	. . . . . 6 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ n =/= m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
245	122, 124, 244	syl2anc 673	. . . . 5 |- ( ( ( ph /\ ( n e. NN /\ m e. NN ) ) /\ -. n = m ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
246	121, 245	pm2.61dan 808	. . . 4 |- ( ( ph /\ ( n e. NN /\ m e. NN ) ) -> ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
247	246	ralrimivva 2814	. . 3 |- ( ph -> A. n e. NN A. m e. NN ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
248		fveq2 5879	. . . 4 |- ( n = m -> ( F ` n ) = ( F ` m ) )
249	248	disjor 4380	. . 3 |- (Disj n e. NN ( F ` n ) <-> A. n e. NN A. m e. NN ( n = m \/ ( ( F ` n ) i^i ( F ` m ) ) = (/) ) )
250	247, 249	sylibr 217	. 2 |- ( ph -> Disj n e. NN ( F ` n ) )
251		nnex 10637	. . . . 5 |- NN e. _V
252	251	mptex 6152	. . . 4 |- ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) ) e. _V
253	26, 252	eqeltri 2545	. . 3 |- F e. _V
254		foeq1 5802	. . . 4 |- ( f = F -> ( f : NN -onto-> ( X u. { (/) } ) <-> F : NN -onto-> ( X u. { (/) } ) ) )
255		simpl 464	. . . . . 6 |- ( ( f = F /\ n e. NN ) -> f = F )
256	255	fveq1d 5881	. . . . 5 |- ( ( f = F /\ n e. NN ) -> ( f ` n ) = ( F ` n ) )
257	256	disjeq2dv 4371	. . . 4 |- ( f = F -> (Disj n e. NN ( f ` n ) <-> Disj n e. NN ( F ` n ) ) )
258	254, 257	anbi12d 725	. . 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 ) ) ) )
259	253, 258	spcev 3127	. 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 ) ) )
260	119, 250, 259	syl2anc 673	1 |- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031   u. cun 3388   i^i cin 3389   C_ wss 3390   (/)c0 3722   ifcif 3872   {csn 3959  Disj wdisj 4366   class class class wbr 4395   |-> cmpt 4454   ran crn 4840   Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308   CCcc 9555   1c1 9558   + caddc 9560   < clt 9693   - cmin 9880   NNcn 10631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-rp 11326

This theorem is referenced by:  nnfoctbdj  38410