Theorem infpssrlem4 8720

Description: Lemma for infpssr 8722. (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 5851	. . . . . . . 8 |- ( c = (/) -> ( G ` c ) = ( G ` (/) ) )
2	1	neeq1d 2682	. . . . . . 7 |- ( c = (/) -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` (/) ) =/= ( G ` b ) ) )
3	2	raleqbi1dv 3014	. . . . . 6 |- ( c = (/) -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) )
4	3	imbi2d 316	. . . . 5 |- ( c = (/) -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) ) )
5		fveq2 5851	. . . . . . . 8 |- ( c = d -> ( G ` c ) = ( G ` d ) )
6	5	neeq1d 2682	. . . . . . 7 |- ( c = d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` d ) =/= ( G ` b ) ) )
7	6	raleqbi1dv 3014	. . . . . 6 |- ( c = d -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. d ( G ` d ) =/= ( G ` b ) ) )
8	7	imbi2d 316	. . . . 5 |- ( c = d -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. d ( G ` d ) =/= ( G ` b ) ) ) )
9		fveq2 5851	. . . . . . . 8 |- ( c = suc d -> ( G ` c ) = ( G ` suc d ) )
10	9	neeq1d 2682	. . . . . . 7 |- ( c = suc d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
11	10	raleqbi1dv 3014	. . . . . 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 316	. . . . 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 5851	. . . . . . . 8 |- ( c = M -> ( G ` c ) = ( G ` M ) )
14	13	neeq1d 2682	. . . . . . 7 |- ( c = M -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` M ) =/= ( G ` b ) ) )
15	14	raleqbi1dv 3014	. . . . . 6 |- ( c = M -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
16	15	imbi2d 316	. . . . 5 |- ( c = M -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) ) )
17		ral0 3880	. . . . . 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 5813	. . . . . . . . . . . . . . . . . 18 |- ( F : B -1-1-onto-> A -> `' F : A -1-1-onto-> B )
21		f1of 5801	. . . . . . . . . . . . . . . . . 18 |- ( `' F : A -1-1-onto-> B -> `' F : A --> B )
22	19, 20, 21	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ph -> `' F : A --> B )
23	22	adantl 466	. . . . . . . . . . . . . . . 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 8719	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : om --> A )
28	27	ffvelrnda 6011	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. om ) -> ( G ` d ) e. A )
29	28	ancoms 453	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ ph ) -> ( G ` d ) e. A )
30	23, 29	ffvelrnd 6012	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ ph ) -> ( `' F ` ( G ` d ) ) e. B )
31	25	eldifbd 3429	. . . . . . . . . . . . . . . 16 |- ( ph -> -. C e. B )
32	31	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ ph ) -> -. C e. B )
33		nelne2 2735	. . . . . . . . . . . . . . 15 |- ( ( ( `' F ` ( G ` d ) ) e. B /\ -. C e. B ) -> ( `' F ` ( G ` d ) ) =/= C )
34	30, 32, 33	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( `' F ` ( G ` d ) ) =/= C )
35	24, 19, 25, 26	infpssrlem2 8718	. . . . . . . . . . . . . . 15 |- ( d e. om -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
36	35	adantr 465	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
37	24, 19, 25, 26	infpssrlem1 8717	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` (/) ) = C )
38	37	adantl 466	. . . . . . . . . . . . . 14 |- ( ( d e. om /\ ph ) -> ( G ` (/) ) = C )
39	34, 36, 38	3netr4d 2710	. . . . . . . . . . . . 13 |- ( ( d e. om /\ ph ) -> ( G ` suc d ) =/= ( G ` (/) ) )
40	39	3adant3 1019	. . . . . . . . . . . 12 |- ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` (/) ) )
41	1	neeq2d 2683	. . . . . . . . . . . 12 |- ( c = (/) -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` (/) ) ) )
42	40, 41	syl5ibr 223	. . . . . . . . . . 11 |- ( c = (/) -> ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` c ) ) )
43	42	adantrd 468	. . . . . . . . . 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 461	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ c e. suc d ) -> c e. suc d )
45		peano2 6706	. . . . . . . . . . . . . . . . 17 |- ( d e. om -> suc d e. om )
46	45	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( d e. om /\ c e. suc d ) -> suc d e. om )
47		elnn 6695	. . . . . . . . . . . . . . . 16 |- ( ( c e. suc d /\ suc d e. om ) -> c e. om )
48	44, 46, 47	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( d e. om /\ c e. suc d ) -> c e. om )
49	48	3ad2antl1 1161	. . . . . . . . . . . . . 14 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> c e. om )
50	49	adantl 466	. . . . . . . . . . . . 13 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c e. om )
51		simpl 457	. . . . . . . . . . . . 13 |- ( ( c =/= (/) /\ ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c =/= (/) )
52		nnsuc 6702	. . . . . . . . . . . . 13 |- ( ( c e. om /\ c =/= (/) ) -> E. b e. om c = suc b )
53	50, 51, 52	syl2anc 661	. . . . . . . . . . . 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 1730	. . . . . . . . . . . . . . . 16 |- F/ b d e. om
55		nfv 1730	. . . . . . . . . . . . . . . 16 |- F/ b ph
56		nfra1 2787	. . . . . . . . . . . . . . . 16 |- F/ b A. b e. d ( G ` d ) =/= ( G ` b )
57	54, 55, 56	nf3an 1960	. . . . . . . . . . . . . . 15 |- F/ b ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) )
58		nfv 1730	. . . . . . . . . . . . . . 15 |- F/ b c e. suc d
59	57, 58	nfan 1958	. . . . . . . . . . . . . 14 |- F/ b ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d )
60		nfv 1730	. . . . . . . . . . . . . 14 |- F/ b ( G ` suc d ) =/= ( G ` c )
61		simpl3 1004	. . . . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d e. om /\ suc b e. suc d ) -> suc b e. suc d )
63		nnord 6693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. om -> Ord d )
64	63	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ suc b e. suc d ) -> Ord d )
65		ordsucelsuc 6642	. . . . . . . . . . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( d e. om /\ suc b e. suc d ) -> b e. d )
68	67	3ad2antl1 1161	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d e. om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) -> b e. d )
69	68	adantrr 717	. . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . 19 |- ( A. b e. d ( G ` d ) =/= ( G ` b ) -> ( b e. d -> ( G ` d ) =/= ( G ` b ) ) )
71	61, 69, 70	sylc 61	. . . . . . . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> `' F : A -1-1-> B )
75	29	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( G ` d ) e. A )
76	27	ffvelrnda 6011	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ b e. om ) -> ( G ` b ) e. A )
77	76	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( G ` b ) e. A )
78		f1fveq 6153	. . . . . . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( `' F ` ( G ` d ) ) = ( `' F ` ( G ` b ) ) <-> ( G ` d ) = ( G ` b ) ) )
80	79	necon3bid 2663	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) <-> ( G ` d ) =/= ( G ` b ) ) )
81	80	biimprd 225	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
82	35	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ b e. om ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
83	24, 19, 25, 26	infpssrlem2 8718	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b e. om -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
84	83	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. om /\ b e. om ) -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
85	82, 84	neeq12d 2684	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( d e. om /\ b e. om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
86	85	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
87	81, 86	sylibrd 236	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d e. om /\ ph ) /\ b e. om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( G ` suc d ) =/= ( G ` suc b ) ) )
88	87	adantrl 716	. . . . . . . . . . . . . . . . . . 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 1157	. . . . . . . . . . . . . . . . . 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 615	. . . . . . . . . . . . . . . 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 2476	. . . . . . . . . . . . . . . . . 18 |- ( c = suc b -> ( c e. suc d <-> suc b e. suc d ) )
93	92	anbi2d 704	. . . . . . . . . . . . . . . . 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 5851	. . . . . . . . . . . . . . . . . . 19 |- ( c = suc b -> ( G ` c ) = ( G ` suc b ) )
95	94	neeq2d 2683	. . . . . . . . . . . . . . . . . 18 |- ( c = suc b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` suc b ) ) )
96	95	imbi2d 316	. . . . . . . . . . . . . . . . 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 320	. . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . 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 83	. . . . . . . . . . . . . 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 2890	. . . . . . . . . . . . 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 466	. . . . . . . . . . . 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 434	. . . . . . . . . 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 2718	. . . . . . . . 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 2820	. . . . . . . 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 5851	. . . . . . . . . 10 |- ( c = b -> ( G ` c ) = ( G ` b ) )
107	106	neeq2d 2683	. . . . . . . . 9 |- ( c = b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
108	107	cbvralv 3036	. . . . . . . 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 198	. . . . . . 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 1198	. . . . . 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 28	. . . . 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 6712	. . . 4 |- ( M e. om -> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
113	112	impcom 430	. . 3 |- ( ( ph /\ M e. om ) -> A. b e. M ( G ` M ) =/= ( G ` b ) )
114		fveq2 5851	. . . . 5 |- ( b = N -> ( G ` b ) = ( G ` N ) )
115	114	neeq2d 2683	. . . 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 1196	1 |- ( ( ph /\ M e. om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 186   /\ wa 369   /\ w3a 976   = wceq 1407   e. wcel 1844   =/= wne 2600   A.wral 2756   E.wrex 2757   \ cdif 3413   C_ wss 3416   (/)c0 3740   `'ccnv 4824   |` cres 4827   Ord word 5411   suc csuc 5414   -->wf 5567   -1-1->wf1 5568   -1-1-onto->wf1o 5570   ` cfv 5571   omcom 6685   reccrdg 7114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-om 6686  df-wrecs 7015  df-recs 7077  df-rdg 7115

This theorem is referenced by:  infpssrlem5  8721