Step |
Hyp |
Ref |
Expression |
1 |
|
onfin2 |
⊢ ω = ( On ∩ Fin ) |
2 |
|
inss2 |
⊢ ( On ∩ Fin ) ⊆ Fin |
3 |
1 2
|
eqsstri |
⊢ ω ⊆ Fin |
4 |
|
peano2 |
⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω ) |
5 |
3 4
|
sselid |
⊢ ( 𝐴 ∈ ω → 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
|
sselid |
⊢ ( ( ( [⊊] 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 ) |