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 ffvelrnda
 |-  ( ( ph /\ d e. _om ) -> ( G ` d ) e. A )
29 28 ancoms
 |-  ( ( d e. _om /\ ph ) -> ( G ` d ) e. A )
30 26 29 ffvelrnd
 |-  ( ( 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 syl5ibr
 |-  ( 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 ffvelrnda
 |-  ( ( 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 ) )