Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
2 |
|
simpr1 |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ ω ) |
3 |
|
ackbij1lem3 |
⊢ ( 𝑐 ∈ ω → 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ) |
4 |
2 3
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ) |
5 |
|
simpr3 |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ¬ 𝑐 ∈ 𝐵 ) |
6 |
|
ackbij1lem1 |
⊢ ( ¬ 𝑐 ∈ 𝐵 → ( 𝐵 ∩ suc 𝑐 ) = ( 𝐵 ∩ 𝑐 ) ) |
7 |
5 6
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐵 ∩ suc 𝑐 ) = ( 𝐵 ∩ 𝑐 ) ) |
8 |
|
inss2 |
⊢ ( 𝐵 ∩ 𝑐 ) ⊆ 𝑐 |
9 |
7 8
|
eqsstrdi |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐵 ∩ suc 𝑐 ) ⊆ 𝑐 ) |
10 |
1
|
ackbij1lem12 |
⊢ ( ( 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∩ suc 𝑐 ) ⊆ 𝑐 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
11 |
4 9 10
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊆ ( 𝐹 ‘ 𝑐 ) ) |
12 |
1
|
ackbij1lem10 |
⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω |
13 |
12
|
ffvelrni |
⊢ ( 𝑐 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝑐 ) ∈ ω ) |
14 |
|
nnon |
⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ω → ( 𝐹 ‘ 𝑐 ) ∈ On ) |
15 |
|
onpsssuc |
⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ On → ( 𝐹 ‘ 𝑐 ) ⊊ suc ( 𝐹 ‘ 𝑐 ) ) |
16 |
4 13 14 15
|
4syl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ⊊ suc ( 𝐹 ‘ 𝑐 ) ) |
17 |
1
|
ackbij1lem14 |
⊢ ( 𝑐 ∈ ω → ( 𝐹 ‘ { 𝑐 } ) = suc ( 𝐹 ‘ 𝑐 ) ) |
18 |
2 17
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ { 𝑐 } ) = suc ( 𝐹 ‘ 𝑐 ) ) |
19 |
18
|
psseq2d |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑐 ) ⊊ ( 𝐹 ‘ { 𝑐 } ) ↔ ( 𝐹 ‘ 𝑐 ) ⊊ suc ( 𝐹 ‘ 𝑐 ) ) ) |
20 |
16 19
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ⊊ ( 𝐹 ‘ { 𝑐 } ) ) |
21 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) |
22 |
|
inss1 |
⊢ ( 𝐴 ∩ suc 𝑐 ) ⊆ 𝐴 |
23 |
1
|
ackbij1lem11 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ suc 𝑐 ) ⊆ 𝐴 ) → ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
24 |
21 22 23
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
25 |
|
ssun1 |
⊢ { 𝑐 } ⊆ ( { 𝑐 } ∪ ( 𝐴 ∩ 𝑐 ) ) |
26 |
|
simpr2 |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐴 ) |
27 |
|
ackbij1lem2 |
⊢ ( 𝑐 ∈ 𝐴 → ( 𝐴 ∩ suc 𝑐 ) = ( { 𝑐 } ∪ ( 𝐴 ∩ 𝑐 ) ) ) |
28 |
26 27
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐴 ∩ suc 𝑐 ) = ( { 𝑐 } ∪ ( 𝐴 ∩ 𝑐 ) ) ) |
29 |
25 28
|
sseqtrrid |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → { 𝑐 } ⊆ ( 𝐴 ∩ suc 𝑐 ) ) |
30 |
1
|
ackbij1lem12 |
⊢ ( ( ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ { 𝑐 } ⊆ ( 𝐴 ∩ suc 𝑐 ) ) → ( 𝐹 ‘ { 𝑐 } ) ⊆ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ) |
31 |
24 29 30
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ { 𝑐 } ) ⊆ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ) |
32 |
20 31
|
psssstrd |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ⊊ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ) |
33 |
11 32
|
sspsstrd |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊊ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ) |
34 |
33
|
pssned |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ≠ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ) |
35 |
34
|
necomd |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ≠ ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ) |
36 |
35
|
neneqd |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵 ) ) → ¬ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ) |