Metamath Proof Explorer

Theorem infpssrlem4

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

Ref Expression
Hypotheses 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 infpssrlem4 
|- ( ( ph /\ M e. _om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )

Proof

Step Hyp Ref Expression
1 infpssrlem.a 
 |-  ( ph -> B C_ A )
2 infpssrlem.c 
 |-  ( ph -> F : B -1-1-onto-> A )
3 infpssrlem.d 
 |-  ( ph -> C e. ( A \ B ) )
4 infpssrlem.e 
 |-  G = ( rec ( `' F , C ) |` _om )
5 fveq2 
 |-  ( c = (/) -> ( G ` c ) = ( G ` (/) ) )
6 5 neeq1d 
 |-  ( c = (/) -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` (/) ) =/= ( G ` b ) ) )
7 6 raleqbi1dv 
 |-  ( c = (/) -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) )
8 7 imbi2d 
 |-  ( c = (/) -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) ) ) )
9 fveq2 
 |-  ( c = d -> ( G ` c ) = ( G ` d ) )
10 9 neeq1d 
 |-  ( c = d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` d ) =/= ( G ` b ) ) )
11 10 raleqbi1dv 
 |-  ( c = d -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. d ( G ` d ) =/= ( G ` b ) ) )
12 11 imbi2d 
 |-  ( c = d -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. d ( G ` d ) =/= ( G ` b ) ) ) )
13 fveq2 
 |-  ( c = suc d -> ( G ` c ) = ( G ` suc d ) )
14 13 neeq1d 
 |-  ( c = suc d -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
15 14 raleqbi1dv 
 |-  ( c = suc d -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) )
16 15 imbi2d 
 |-  ( c = suc d -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) ) )
17 fveq2 
 |-  ( c = M -> ( G ` c ) = ( G ` M ) )
18 17 neeq1d 
 |-  ( c = M -> ( ( G ` c ) =/= ( G ` b ) <-> ( G ` M ) =/= ( G ` b ) ) )
19 18 raleqbi1dv 
 |-  ( c = M -> ( A. b e. c ( G ` c ) =/= ( G ` b ) <-> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
20 19 imbi2d 
 |-  ( c = M -> ( ( ph -> A. b e. c ( G ` c ) =/= ( G ` b ) ) <-> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) ) )
21 ral0 
 |-  A. b e. (/) ( G ` (/) ) =/= ( G ` b )
22 21 a1i 
 |-  ( ph -> A. b e. (/) ( G ` (/) ) =/= ( G ` b ) )
23 f1ocnv 
 |-  ( F : B -1-1-onto-> A -> `' F : A -1-1-onto-> B )
24 f1of 
 |-  ( `' F : A -1-1-onto-> B -> `' F : A --> B )
25 2 23 24 3syl 
 |-  ( ph -> `' F : A --> B )
26 25 adantl 
 |-  ( ( d e. _om /\ ph ) -> `' F : A --> B )
27 1 2 3 4 infpssrlem3 
 |-  ( ph -> G : _om --> A )
28 27 ffvelcdmda 
 |-  ( ( ph /\ d e. _om ) -> ( G ` d ) e. A )
29 28 ancoms 
 |-  ( ( d e. _om /\ ph ) -> ( G ` d ) e. A )
30 26 29 ffvelcdmd 
 |-  ( ( d e. _om /\ ph ) -> ( `' F ` ( G ` d ) ) e. B )
31 3 eldifbd 
 |-  ( ph -> -. C e. B )
32 31 adantl 
 |-  ( ( d e. _om /\ ph ) -> -. C e. B )
33 nelne2 
 |-  ( ( ( `' F ` ( G ` d ) ) e. B /\ -. C e. B ) -> ( `' F ` ( G ` d ) ) =/= C )
34 30 32 33 syl2anc 
 |-  ( ( d e. _om /\ ph ) -> ( `' F ` ( G ` d ) ) =/= C )
35 1 2 3 4 infpssrlem2 
 |-  ( d e. _om -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
36 35 adantr 
 |-  ( ( d e. _om /\ ph ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
37 1 2 3 4 infpssrlem1 
 |-  ( ph -> ( G ` (/) ) = C )
38 37 adantl 
 |-  ( ( d e. _om /\ ph ) -> ( G ` (/) ) = C )
39 34 36 38 3netr4d 
 |-  ( ( d e. _om /\ ph ) -> ( G ` suc d ) =/= ( G ` (/) ) )
40 39 3adant3 
 |-  ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` (/) ) )
41 5 neeq2d 
 |-  ( c = (/) -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` (/) ) ) )
42 40 41 imbitrrid 
 |-  ( c = (/) -> ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( G ` suc d ) =/= ( G ` c ) ) )
43 42 adantrd 
 |-  ( c = (/) -> ( ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( G ` suc d ) =/= ( G ` c ) ) )
44 simpr 
 |-  ( ( d e. _om /\ c e. suc d ) -> c e. suc d )
45 peano2 
 |-  ( d e. _om -> suc d e. _om )
46 45 adantr 
 |-  ( ( d e. _om /\ c e. suc d ) -> suc d e. _om )
47 elnn 
 |-  ( ( c e. suc d /\ suc d e. _om ) -> c e. _om )
48 44 46 47 syl2anc 
 |-  ( ( d e. _om /\ c e. suc d ) -> c e. _om )
49 48 3ad2antl1 
 |-  ( ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> c e. _om )
50 49 adantl 
 |-  ( ( c =/= (/) /\ ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c e. _om )
51 simpl 
 |-  ( ( c =/= (/) /\ ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) ) -> c =/= (/) )
52 nnsuc 
 |-  ( ( c e. _om /\ c =/= (/) ) -> E. b e. _om c = suc b )
53 50 51 52 syl2anc 
 |-  ( ( 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 
 |-  F/ b d e. _om
55 nfv 
 |-  F/ b ph
56 nfra1 
 |-  F/ b A. b e. d ( G ` d ) =/= ( G ` b )
57 54 55 56 nf3an 
 |-  F/ b ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) )
58 nfv 
 |-  F/ b c e. suc d
59 57 58 nfan 
 |-  F/ b ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d )
60 nfv 
 |-  F/ b ( G ` suc d ) =/= ( G ` c )
61 simpl3 
 |-  ( ( ( 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 
 |-  ( ( d e. _om /\ suc b e. suc d ) -> suc b e. suc d )
63 nnord 
 |-  ( d e. _om -> Ord d )
64 63 adantr 
 |-  ( ( d e. _om /\ suc b e. suc d ) -> Ord d )
65 ordsucelsuc 
 |-  ( Ord d -> ( b e. d <-> suc b e. suc d ) )
66 64 65 syl 
 |-  ( ( d e. _om /\ suc b e. suc d ) -> ( b e. d <-> suc b e. suc d ) )
67 62 66 mpbird 
 |-  ( ( d e. _om /\ suc b e. suc d ) -> b e. d )
68 67 3ad2antl1 
 |-  ( ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ suc b e. suc d ) -> b e. d )
69 68 adantrr 
 |-  ( ( ( 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 
 |-  ( A. b e. d ( G ` d ) =/= ( G ` b ) -> ( b e. d -> ( G ` d ) =/= ( G ` b ) ) )
71 61 69 70 sylc 
 |-  ( ( ( 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 
 |-  ( `' F : A -1-1-onto-> B -> `' F : A -1-1-> B )
73 2 23 72 3syl 
 |-  ( ph -> `' F : A -1-1-> B )
74 73 ad2antlr 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> `' F : A -1-1-> B )
75 29 adantr 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( G ` d ) e. A )
76 27 ffvelcdmda 
 |-  ( ( ph /\ b e. _om ) -> ( G ` b ) e. A )
77 76 adantll 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( G ` b ) e. A )
78 f1fveq 
 |-  ( ( `' 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 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( ( `' F ` ( G ` d ) ) = ( `' F ` ( G ` b ) ) <-> ( G ` d ) = ( G ` b ) ) )
80 79 necon3bid 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) <-> ( G ` d ) =/= ( G ` b ) ) )
81 80 biimprd 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
82 35 adantr 
 |-  ( ( d e. _om /\ b e. _om ) -> ( G ` suc d ) = ( `' F ` ( G ` d ) ) )
83 1 2 3 4 infpssrlem2 
 |-  ( b e. _om -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
84 83 adantl 
 |-  ( ( d e. _om /\ b e. _om ) -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
85 82 84 neeq12d 
 |-  ( ( d e. _om /\ b e. _om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
86 85 adantlr 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( ( G ` suc d ) =/= ( G ` suc b ) <-> ( `' F ` ( G ` d ) ) =/= ( `' F ` ( G ` b ) ) ) )
87 81 86 sylibrd 
 |-  ( ( ( d e. _om /\ ph ) /\ b e. _om ) -> ( ( G ` d ) =/= ( G ` b ) -> ( G ` suc d ) =/= ( G ` suc b ) ) )
88 87 adantrl 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( c = suc b -> ( c e. suc d <-> suc b e. suc d ) )
93 92 anbi2d 
 |-  ( 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 
 |-  ( c = suc b -> ( G ` c ) = ( G ` suc b ) )
95 94 neeq2d 
 |-  ( c = suc b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` suc b ) ) )
96 95 imbi2d 
 |-  ( c = suc b -> ( ( b e. _om -> ( G ` suc d ) =/= ( G ` c ) ) <-> ( b e. _om -> ( G ` suc d ) =/= ( G ` suc b ) ) ) )
97 93 96 imbi12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) /\ c e. suc d ) -> ( G ` suc d ) =/= ( G ` c ) )
105 104 ralrimiva 
 |-  ( ( d e. _om /\ ph /\ A. b e. d ( G ` d ) =/= ( G ` b ) ) -> A. c e. suc d ( G ` suc d ) =/= ( G ` c ) )
106 fveq2 
 |-  ( c = b -> ( G ` c ) = ( G ` b ) )
107 106 neeq2d 
 |-  ( c = b -> ( ( G ` suc d ) =/= ( G ` c ) <-> ( G ` suc d ) =/= ( G ` b ) ) )
108 107 cbvralvw 
 |-  ( A. c e. suc d ( G ` suc d ) =/= ( G ` c ) <-> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) )
109 105 108 sylib 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( d e. _om -> ( ( ph -> A. b e. d ( G ` d ) =/= ( G ` b ) ) -> ( ph -> A. b e. suc d ( G ` suc d ) =/= ( G ` b ) ) ) )
112 8 12 16 20 22 111 finds 
 |-  ( M e. _om -> ( ph -> A. b e. M ( G ` M ) =/= ( G ` b ) ) )
113 112 impcom 
 |-  ( ( ph /\ M e. _om ) -> A. b e. M ( G ` M ) =/= ( G ` b ) )
114 fveq2 
 |-  ( b = N -> ( G ` b ) = ( G ` N ) )
115 114 neeq2d 
 |-  ( b = N -> ( ( G ` M ) =/= ( G ` b ) <-> ( G ` M ) =/= ( G ` N ) ) )
116 115 rspccv 
 |-  ( A. b e. M ( G ` M ) =/= ( G ` b ) -> ( N e. M -> ( G ` M ) =/= ( G ` N ) ) )
117 113 116 syl 
 |-  ( ( ph /\ M e. _om ) -> ( N e. M -> ( G ` M ) =/= ( G ` N ) ) )
118 117 3impia 
 |-  ( ( ph /\ M e. _om /\ N e. M ) -> ( G ` M ) =/= ( G ` N ) )