Theorem infpssrlem4 8767

Description: Lemma for infpssr 8769. (Contributed by Stefan O'Rear, 30-Oct-2014.)

Hypotheses

Ref	Expression
infpssrlem.a	|- ( ph -> B C_ A )
infpssrlem.c	|- ( ph -> F : B -1-1-onto-> A )
infpssrlem.d	|- ( ph -> C e. ( A \ B ) )
infpssrlem.e	|- G = ( rec ( `' F , C ) |` om )

Assertion

Ref	Expression
infpssrlem4	|- ( ( ph /\ M e. om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )

Proof of Theorem infpssrlem4

Dummy variables b c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5892	. . . . . . . 8 |- ( c = (/) -> ( G ` c ) = ( G ` (/) ) )
2	1	neeq1d 2695	. . . . . . 7 |- ( c = (/) -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` (/) ) =/= ( G ` b ) ) )
3	2	raleqbi1dv 3007	. . . . . 6 |- ( c = (/) -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) )
4	3	imbi2d 322	. . . . 5 |- ( c = (/) -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) ) )
5		fveq2 5892	. . . . . . . 8 |- ( c = d -> ( G ` c ) = ( G ` d ) )
6	5	neeq1d 2695	. . . . . . 7 |- ( c = d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` d ) =/= ( G ` b ) ) )
7	6	raleqbi1dv 3007	. . . . . 6 |- ( c = d -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. d ( G ` d ) =/= ( G ` b ) ) )
8	7	imbi2d 322	. . . . 5 |- ( c = d -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. d ( G ` d ) =/= ( G ` b ) ) ) )
9		fveq2 5892	. . . . . . . 8 |- ( c = suc d -> ( G ` c ) = ( G ` suc d ) )
10	9	neeq1d 2695	. . . . . . 7 |- ( c = suc d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
11	10	raleqbi1dv 3007	. . . . . 6 |- ( c = suc d -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) )
12	11	imbi2d 322	. . . . 5 |- ( c = suc d -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) ) )
13		fveq2 5892	. . . . . . . 8 |- ( c = M -> ( G ` c ) = ( G ` M ) )
14	13	neeq1d 2695	. . . . . . 7 |- ( c = M -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` M ) =/= ( G ` b ) ) )
15	14	raleqbi1dv 3007	. . . . . 6 |- ( c = M -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
16	15	imbi2d 322	. . . . 5 |- ( c = M -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) ) )
17		ral0 3886	. . . . . 6 |- A. b e. (/) ( G ` (/) ) =/= ( G ` b )
18	17	a1i 11	. . . . 5 |- ( ph -> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) )
19		infpssrlem.c	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F : B -1-1-onto-> A )
20		f1ocnv 5853	. . . . . . . . . . . . . . . . . 18 |- ( F : B -1-1-onto-> A -> `' F : A -1-1-onto-> B )
21		f1of 5841	. . . . . . . . . . . . . . . . . 18 |- ( `' F : A -1-1-onto-> B -> `' F : A --> B )
22	19, 20, 21	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ph -> `' F : A --> B )
23	22	adantl 472	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ ph ) -> `' F : A --> B )
24		infpssrlem.a	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> B C_ A )
25		infpssrlem.d	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> C e. ( A \ B ) )
26		infpssrlem.e	. . . . . . . . . . . . . . . . . . 19 |- G = ( rec ( `' F , C ) |` om )
27	24, 19, 25, 26	infpssrlem3 8766	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : om --> A )
28	27	ffvelrnda 6050	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. om ) -> ( G ` d ) e. A )
29	28	ancoms 459	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ ph ) -> ( G ` d ) e. A )
30	23, 29	ffvelrnd 6051	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ ph ) -> ( `' F ` ( G ` d ) ) e. B )
31	25	eldifbd 3429	. . . . . . . . . . . . . . . 16 |- ( ph -> -. C e. B )
32	31	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ ph ) -> -. C e. B )
33		nelne2 2733	. . . . . . . . . . . . . . 15 |- ( ( ( `' F ` ( G ` d ) ) e. B /\ -. C e. B ) -> ( `' F ` ( G ` d ) ) =/= C )
34	30, 32, 33	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( `' F ` ( G ` d ) ) =/= C )
35	24, 19, 25, 26	infpssrlem2 8765	. . . . . . . . . . . . . . 15 |- ( d e. om -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
36	35	adantr 471	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
37	24, 19, 25, 26	infpssrlem1 8764	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (/) ) = C )
38	37	adantl 472	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( G ` (/) ) = C )
39	34, 36, 38	3netr4d 2713	. . . . . . . . . . . . 13 |- ( ( d e. om /\ ph ) -> ( G ` suc d ) =/= ( G ` (/) ) )
40	39	3adant3 1034	. . . . . . . . . . . 12 |- ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` (/) ) )
41	1	neeq2d 2696	. . . . . . . . . . . 12 |- ( c = (/) -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` (/) ) ) )
42	40, 41	syl5ibr 229	. . . . . . . . . . 11 |- ( c = (/) -> ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` c ) ) )
43	42	adantrd 474	. . . . . . . . . 10 |- ( c = (/) -> ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( G ` suc d ) =/= ( G ` c ) ) )
44		simpr 467	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ c e. suc d ) -> c e. suc d )
45		peano2 6745	. . . . . . . . . . . . . . . . 17 |- ( d e. om -> suc d e. om )
46	45	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ c e. suc d ) -> suc d e. om )
47		elnn 6734	. . . . . . . . . . . . . . . 16 |- ( ( c e. suc d /\ suc d e. om ) -> c e. om )
48	44, 46, 47	syl2anc 671	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ c e. suc d ) -> c e. om )
49	48	3ad2antl1 1176	. . . . . . . . . . . . . 14 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> c e. om )
50	49	adantl 472	. . . . . . . . . . . . 13 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c e. om )
51		simpl 463	. . . . . . . . . . . . 13 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c =/= (/) )
52		nnsuc 6741	. . . . . . . . . . . . 13 |- ( ( c e. om /\ c =/= (/) ) -> E. b e. om c = suc b )
53	50, 51, 52	syl2anc 671	. . . . . . . . . . . 12 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> E. b e. om c = suc b )
54		nfv 1772	. . . . . . . . . . . . . . . 16 |- F/ b d e. om
55		nfv 1772	. . . . . . . . . . . . . . . 16 |- F/ b ph
56		nfra1 2781	. . . . . . . . . . . . . . . 16 |- F/ b A. b e. d ( G ` d ) =/= ( G ` b )
57	54, 55, 56	nf3an 2024	. . . . . . . . . . . . . . 15 |- F/ b ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) )
58		nfv 1772	. . . . . . . . . . . . . . 15 |- F/ b c e. suc d
59	57, 58	nfan 2022	. . . . . . . . . . . . . 14 |- F/ b ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d )
60		nfv 1772	. . . . . . . . . . . . . 14 |- F/ b ( G ` suc d ) =/= ( G ` c )
61		simpl3 1019	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ ( suc b e. suc d /\ b e. om ) ) -> A. b e. d ( G ` d ) =/= ( G ` b ) )
62		simpr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d e. om /\ suc b e. suc d ) -> suc b e. suc d )
63		nnord 6732	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. om -> Ord d )
64	63	adantr 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ suc b e. suc d ) -> Ord d )
65		ordsucelsuc 6681	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Ord d -> ( b e. d <-> suc b e. suc d ) )
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d e. om /\ suc b e. suc d ) -> ( b e. d <-> suc b e. suc d ) )
67	62, 66	mpbird 240	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( d e. om /\ suc b e. suc d ) -> b e. d )
68	67	3ad2antl1 1176	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) -> b e. d )
69	68	adantrr 728	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ ( suc b e. suc d /\ b e. om ) ) -> b e. d )
70		rsp 2766	. . . . . . . . . . . . . . . . . . 19 |- ( A. b e. d ( G ` d ) =/= ( G ` b ) -> ( b e. d -> ( G ` d ) =/= ( G ` b ) ) )
71	61, 69, 70	sylc 62	. . . . . . . . . . . . . . . . . 18 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ ( suc b e. suc d /\ b e. om ) ) -> ( G ` d ) =/= ( G ` b ) )
72		f1of1 5840	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( `' F : A -1-1-onto-> B -> `' F : A -1-1-> B )
73	19, 20, 72	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> `' F : A -1-1-> B )
74	73	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> `' F : A -1-1-> B )
75	29	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( G ` d ) e. A )
76	27	ffvelrnda 6050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ b e. om ) -> ( G ` b ) e. A )
77	76	adantll 725	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( G ` b ) e. A )
78		f1fveq 6193	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( `' F : A -1-1-> B /\ ( ( G ` d ) e. A /\ ( G ` b ) e. A ) ) -> ( ( `' F ` ( G ` d ) ) = ( `' F ` ( G ` b ) ) <-> ( G ` d ) = ( G ` b ) ) )
79	74, 75, 77, 78	syl12anc 1274	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( `' F ` ( G ` d ) ) = ( `' F ` ( G ` b ) ) <-> ( G ` d ) = ( G ` b ) ) )
80	79	necon3bid 2680	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) <-> ( G ` d ) =/= ( G ` b ) ) )
81	80	biimprd 231	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
82	35	adantr 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ b e. om ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
83	24, 19, 25, 26	infpssrlem2 8765	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b e. om -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
84	83	adantl 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ b e. om ) -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
85	82, 84	neeq12d 2697	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d e. om /\ b e. om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
86	85	adantlr 726	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
87	81, 86	sylibrd 242	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( G ` suc d ) =/= ( G ` suc b ) ) )
88	87	adantrl 727	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( d e. om /\ ph ) /\ ( suc b e. suc d /\ b e. om ) ) -> ( ( G ` d ) =/= ( G ` b ) -> ( G ` suc d ) =/= ( G ` suc b ) ) )
89	88	3adantl3 1172	. . . . . . . . . . . . . . . . . 18 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ ( suc b e. suc d /\ b e. om ) ) -> ( ( G ` d ) =/= ( G ` b ) -> ( G ` suc d ) =/= ( G ` suc b ) ) )
90	71, 89	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ ( suc b e. suc d /\ b e. om ) ) -> ( G ` suc d ) =/= ( G ` suc b ) )
91	90	expr 624	. . . . . . . . . . . . . . . 16 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) -> ( b e. om -> ( G ` suc d ) =/= ( G ` suc b ) ) )
92		eleq1 2528	. . . . . . . . . . . . . . . . . 18 |- ( c = suc b -> ( c e. suc d <-> suc b e. suc d ) )
93	92	anbi2d 715	. . . . . . . . . . . . . . . . 17 |- ( c = suc b -> ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) <-> ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) ) )
94		fveq2 5892	. . . . . . . . . . . . . . . . . . 19 |- ( c = suc b -> ( G ` c ) = ( G ` suc b ) )
95	94	neeq2d 2696	. . . . . . . . . . . . . . . . . 18 |- ( c = suc b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` suc b ) ) )
96	95	imbi2d 322	. . . . . . . . . . . . . . . . 17 |- ( c = suc b -> ( ( b e. om -> ( G ` suc d ) =/= ( G ` c ) ) <-> ( b e. om -> ( G ` suc d ) =/= ( G ` suc b ) ) ) )
97	93, 96	imbi12d 326	. . . . . . . . . . . . . . . 16 |- ( c = suc b -> ( ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( b e. om -> ( G ` suc d ) =/= ( G ` c ) ) ) <-> ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) -> ( b e. om -> ( G ` suc d ) =/= ( G ` suc b ) ) ) ) )
98	91, 97	mpbiri 241	. . . . . . . . . . . . . . 15 |- ( c = suc b -> ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( b e. om -> ( G ` suc d ) =/= ( G ` c ) ) ) )
99	98	com3l 84	. . . . . . . . . . . . . 14 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( b e. om -> ( c = suc b -> ( G ` suc d ) =/= ( G ` c ) ) ) )
100	59, 60, 99	rexlimd 2883	. . . . . . . . . . . . 13 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( E. b e. om c = suc b -> ( G ` suc d ) =/= ( G ` c ) ) )
101	100	adantl 472	. . . . . . . . . . . 12 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> ( E. b e. om c = suc b -> ( G ` suc d ) =/= ( G ` c ) ) )
102	53, 101	mpd 15	. . . . . . . . . . 11 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> ( G ` suc d ) =/= ( G ` c ) )
103	102	ex 440	. . . . . . . . . 10 |- ( c =/= (/) -> ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( G ` suc d ) =/= ( G ` c ) ) )
104	43, 103	pm2.61ine 2719	. . . . . . . . 9 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( G ` suc d ) =/= ( G ` c ) )
105	104	ralrimiva 2814	. . . . . . . 8 |- ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> A. c e. suc d ( G ` suc d ) =/= ( G ` c ) )
106		fveq2 5892	. . . . . . . . . 10 |- ( c = b -> ( G ` c ) = ( G ` b ) )
107	106	neeq2d 2696	. . . . . . . . 9 |- ( c = b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
108	107	cbvralv 3031	. . . . . . . 8 |- ( A. c e. suc d ( G ` suc d ) =/= ( G ` c ) <-> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) )
109	105, 108	sylib 201	. . . . . . 7 |- ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) )
110	109	3exp 1214	. . . . . 6 |- ( d e. om -> ( ph -> ( A. b e. d ( G ` d ) =/= ( G ` b ) -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) ) )
111	110	a2d 29	. . . . 5 |- ( d e. om -> ( ( ph -> A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( ph -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) ) )
112	4, 8, 12, 16, 18, 111	finds 6751	. . . 4 |- ( M e. om -> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
113	112	impcom 436	. . 3 |- ( ( ph /\ M e. om ) -> A. b e. M ( G ` M ) =/= ( G ` b ) )
114		fveq2 5892	. . . . 5 |- ( b = N -> ( G ` b ) = ( G ` N ) )
115	114	neeq2d 2696	. . . 4 |- ( b = N -> ( ( G ` M ) =/= ( G ` b ) <-> ( G ` M ) =/= ( G ` N ) ) )
116	115	rspccv 3159	. . 3 |- ( A. b e. M ( G ` M ) =/= ( G ` b ) -> ( N e. M -> ( G ` M ) =/= ( G ` N ) ) )
117	113, 116	syl 17	. 2 |- ( ( ph /\ M e. om ) -> ( N e. M -> ( G ` M ) =/= ( G ` N ) ) )
118	117	3impia 1212	1 |- ( ( ph /\ M e. om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   A.wral 2749   E.wrex 2750   \ cdif 3413   C_ wss 3416   (/)c0 3743   `'ccnv 4855   |` cres 4858   Ord word 5445   suc csuc 5448   -->wf 5601   -1-1->wf1 5602   -1-1-onto->wf1o 5604   ` cfv 5605   omcom 6724   reccrdg 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159

This theorem is referenced by:  infpssrlem5  8768