Step |
Hyp |
Ref |
Expression |
1 |
|
cardf2 |
⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On |
2 |
|
ffun |
⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card ) |
3 |
1 2
|
ax-mp |
⊢ Fun card |
4 |
|
r1fnon |
⊢ 𝑅1 Fn On |
5 |
|
fnfun |
⊢ ( 𝑅1 Fn On → Fun 𝑅1 ) |
6 |
4 5
|
ax-mp |
⊢ Fun 𝑅1 |
7 |
|
funco |
⊢ ( ( Fun card ∧ Fun 𝑅1 ) → Fun ( card ∘ 𝑅1 ) ) |
8 |
3 6 7
|
mp2an |
⊢ Fun ( card ∘ 𝑅1 ) |
9 |
|
funfn |
⊢ ( Fun ( card ∘ 𝑅1 ) ↔ ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 ) ) |
10 |
8 9
|
mpbi |
⊢ ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 ) |
11 |
|
rnco |
⊢ ran ( card ∘ 𝑅1 ) = ran ( card ↾ ran 𝑅1 ) |
12 |
|
resss |
⊢ ( card ↾ ran 𝑅1 ) ⊆ card |
13 |
12
|
rnssi |
⊢ ran ( card ↾ ran 𝑅1 ) ⊆ ran card |
14 |
|
frn |
⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → ran card ⊆ On ) |
15 |
1 14
|
ax-mp |
⊢ ran card ⊆ On |
16 |
13 15
|
sstri |
⊢ ran ( card ↾ ran 𝑅1 ) ⊆ On |
17 |
11 16
|
eqsstri |
⊢ ran ( card ∘ 𝑅1 ) ⊆ On |
18 |
|
df-f |
⊢ ( ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On ↔ ( ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 ) ∧ ran ( card ∘ 𝑅1 ) ⊆ On ) ) |
19 |
10 17 18
|
mpbir2an |
⊢ ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On |
20 |
|
dmco |
⊢ dom ( card ∘ 𝑅1 ) = ( ◡ 𝑅1 “ dom card ) |
21 |
20
|
feq2i |
⊢ ( ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On ↔ ( card ∘ 𝑅1 ) : ( ◡ 𝑅1 “ dom card ) ⟶ On ) |
22 |
19 21
|
mpbi |
⊢ ( card ∘ 𝑅1 ) : ( ◡ 𝑅1 “ dom card ) ⟶ On |
23 |
|
elpreima |
⊢ ( 𝑅1 Fn On → ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑥 ∈ On ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) ) ) |
24 |
4 23
|
ax-mp |
⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑥 ∈ On ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) ) |
25 |
24
|
simplbi |
⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → 𝑥 ∈ On ) |
26 |
|
onelon |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On ) |
27 |
25 26
|
sylan |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On ) |
28 |
24
|
simprbi |
⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) |
29 |
28
|
adantr |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) |
30 |
|
r1ord2 |
⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) ) |
31 |
30
|
imp |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) |
32 |
25 31
|
sylan |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) |
33 |
|
ssnum |
⊢ ( ( ( 𝑅1 ‘ 𝑥 ) ∈ dom card ∧ ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) → ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) |
34 |
29 32 33
|
syl2anc |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) |
35 |
|
elpreima |
⊢ ( 𝑅1 Fn On → ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑦 ∈ On ∧ ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) ) ) |
36 |
4 35
|
ax-mp |
⊢ ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑦 ∈ On ∧ ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) ) |
37 |
27 34 36
|
sylanbrc |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ) |
38 |
37
|
rgen2 |
⊢ ∀ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) |
39 |
|
dftr5 |
⊢ ( Tr ( ◡ 𝑅1 “ dom card ) ↔ ∀ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ) |
40 |
38 39
|
mpbir |
⊢ Tr ( ◡ 𝑅1 “ dom card ) |
41 |
|
cnvimass |
⊢ ( ◡ 𝑅1 “ dom card ) ⊆ dom 𝑅1 |
42 |
|
dffn2 |
⊢ ( 𝑅1 Fn On ↔ 𝑅1 : On ⟶ V ) |
43 |
4 42
|
mpbi |
⊢ 𝑅1 : On ⟶ V |
44 |
43
|
fdmi |
⊢ dom 𝑅1 = On |
45 |
41 44
|
sseqtri |
⊢ ( ◡ 𝑅1 “ dom card ) ⊆ On |
46 |
|
epweon |
⊢ E We On |
47 |
|
wess |
⊢ ( ( ◡ 𝑅1 “ dom card ) ⊆ On → ( E We On → E We ( ◡ 𝑅1 “ dom card ) ) ) |
48 |
45 46 47
|
mp2 |
⊢ E We ( ◡ 𝑅1 “ dom card ) |
49 |
|
df-ord |
⊢ ( Ord ( ◡ 𝑅1 “ dom card ) ↔ ( Tr ( ◡ 𝑅1 “ dom card ) ∧ E We ( ◡ 𝑅1 “ dom card ) ) ) |
50 |
40 48 49
|
mpbir2an |
⊢ Ord ( ◡ 𝑅1 “ dom card ) |
51 |
|
r1sdom |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) |
52 |
25 51
|
sylan |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) |
53 |
|
cardsdom2 |
⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ∈ dom card ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) |
54 |
34 29 53
|
syl2anc |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) ) |
55 |
52 54
|
mpbird |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ) |
56 |
|
fvco2 |
⊢ ( ( 𝑅1 Fn On ∧ 𝑦 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
57 |
4 27 56
|
sylancr |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) |
58 |
25
|
adantr |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ On ) |
59 |
|
fvco2 |
⊢ ( ( 𝑅1 Fn On ∧ 𝑥 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) = ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ) |
60 |
4 58 59
|
sylancr |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) = ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ) |
61 |
55 57 60
|
3eltr4d |
⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) ) |
62 |
61
|
ex |
⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → ( 𝑦 ∈ 𝑥 → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) ) ) |
63 |
62
|
adantl |
⊢ ( ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ) → ( 𝑦 ∈ 𝑥 → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) ) ) |
64 |
22 50 63 20
|
issmo |
⊢ Smo ( card ∘ 𝑅1 ) |