| Step |
Hyp |
Ref |
Expression |
| 1 |
|
onfin2 |
⊢ ω = ( On ∩ Fin ) |
| 2 |
|
inss2 |
⊢ ( On ∩ Fin ) ⊆ Fin |
| 3 |
1 2
|
eqsstri |
⊢ ω ⊆ Fin |
| 4 |
|
peano2 |
⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω ) |
| 5 |
3 4
|
sseldi |
⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ Fin ) |
| 6 |
5
|
3ad2ant3 |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → suc 𝐴 ∈ Fin ) |
| 7 |
4
|
3ad2ant3 |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → suc 𝐴 ∈ ω ) |
| 8 |
|
breq1 |
⊢ ( 𝑏 = 𝑐 → ( 𝑏 ≼ 𝐴 ↔ 𝑐 ≼ 𝐴 ) ) |
| 9 |
8
|
elrab |
⊢ ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ↔ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) |
| 10 |
|
simprr |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ≼ 𝐴 ) |
| 11 |
|
simpl2 |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑋 ⊆ Fin ) |
| 12 |
|
simprl |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ 𝑋 ) |
| 13 |
11 12
|
sseldd |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ Fin ) |
| 14 |
|
finnum |
⊢ ( 𝑐 ∈ Fin → 𝑐 ∈ dom card ) |
| 15 |
13 14
|
syl |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝑐 ∈ dom card ) |
| 16 |
|
simpl3 |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ ω ) |
| 17 |
3 16
|
sseldi |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ Fin ) |
| 18 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
| 19 |
17 18
|
syl |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → 𝐴 ∈ dom card ) |
| 20 |
|
carddom2 |
⊢ ( ( 𝑐 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝑐 ≼ 𝐴 ) ) |
| 21 |
15 19 20
|
syl2anc |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ 𝑐 ≼ 𝐴 ) ) |
| 22 |
10 21
|
mpbird |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) ) → ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ) |
| 23 |
22
|
ex |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) → ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ) ) |
| 24 |
|
cardnn |
⊢ ( 𝐴 ∈ ω → ( card ‘ 𝐴 ) = 𝐴 ) |
| 25 |
24
|
sseq2d |
⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ⊆ 𝐴 ) ) |
| 26 |
|
cardon |
⊢ ( card ‘ 𝑐 ) ∈ On |
| 27 |
|
nnon |
⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On ) |
| 28 |
|
onsssuc |
⊢ ( ( ( card ‘ 𝑐 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( card ‘ 𝑐 ) ⊆ 𝐴 ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 29 |
26 27 28
|
sylancr |
⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ 𝐴 ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 30 |
25 29
|
bitrd |
⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 31 |
30
|
3ad2ant3 |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( card ‘ 𝑐 ) ⊆ ( card ‘ 𝐴 ) ↔ ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 32 |
23 31
|
sylibd |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑐 ≼ 𝐴 ) → ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 33 |
9 32
|
syl5bi |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → ( card ‘ 𝑐 ) ∈ suc 𝐴 ) ) |
| 34 |
|
elrabi |
⊢ ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → 𝑐 ∈ 𝑋 ) |
| 35 |
|
elrabi |
⊢ ( 𝑑 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } → 𝑑 ∈ 𝑋 ) |
| 36 |
|
ssel |
⊢ ( 𝑋 ⊆ Fin → ( 𝑐 ∈ 𝑋 → 𝑐 ∈ Fin ) ) |
| 37 |
|
ssel |
⊢ ( 𝑋 ⊆ Fin → ( 𝑑 ∈ 𝑋 → 𝑑 ∈ Fin ) ) |
| 38 |
36 37
|
anim12d |
⊢ ( 𝑋 ⊆ Fin → ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) ) |
| 39 |
38
|
imp |
⊢ ( ( 𝑋 ⊆ Fin ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) |
| 40 |
39
|
3ad2antl2 |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) |
| 41 |
|
sorpssi |
⊢ ( ( [⊊] Or 𝑋 ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) |
| 42 |
41
|
3ad2antl1 |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) |
| 43 |
|
finnum |
⊢ ( 𝑑 ∈ Fin → 𝑑 ∈ dom card ) |
| 44 |
|
carden2 |
⊢ ( ( 𝑐 ∈ dom card ∧ 𝑑 ∈ dom card ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) ) |
| 45 |
14 43 44
|
syl2an |
⊢ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) ) |
| 46 |
45
|
adantr |
⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 ≈ 𝑑 ) ) |
| 47 |
|
fin23lem25 |
⊢ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 ↔ 𝑐 = 𝑑 ) ) |
| 48 |
47
|
3expa |
⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 ↔ 𝑐 = 𝑑 ) ) |
| 49 |
48
|
biimpd |
⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( 𝑐 ≈ 𝑑 → 𝑐 = 𝑑 ) ) |
| 50 |
46 49
|
sylbid |
⊢ ( ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( 𝑐 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑐 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) |
| 51 |
40 42 50
|
syl2anc |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) |
| 52 |
|
fveq2 |
⊢ ( 𝑐 = 𝑑 → ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ) |
| 53 |
51 52
|
impbid1 |
⊢ ( ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) ) |
| 54 |
53
|
ex |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) ) ) |
| 55 |
34 35 54
|
syl2ani |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( ( 𝑐 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∧ 𝑑 ∈ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ) → ( ( card ‘ 𝑐 ) = ( card ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) ) ) |
| 56 |
33 55
|
dom2d |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → ( suc 𝐴 ∈ ω → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 ) ) |
| 57 |
7 56
|
mpd |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 ) |
| 58 |
|
domfi |
⊢ ( ( suc 𝐴 ∈ Fin ∧ { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ≼ suc 𝐴 ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∈ Fin ) |
| 59 |
6 57 58
|
syl2anc |
⊢ ( ( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω ) → { 𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴 } ∈ Fin ) |