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 ) ) |