| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 2 |
|
inss1 |
⊢ ( 𝒫 ω ∩ Fin ) ⊆ 𝒫 ω |
| 3 |
2
|
sseli |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ 𝒫 ω ) |
| 4 |
3
|
elpwid |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ⊆ ω ) |
| 5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐴 ⊆ ω ) |
| 6 |
2
|
sseli |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ 𝒫 ω ) |
| 7 |
6
|
elpwid |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ⊆ ω ) |
| 8 |
7
|
adantl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ⊆ ω ) |
| 9 |
5 8
|
unssd |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ω ) |
| 10 |
|
inss2 |
⊢ ( 𝒫 ω ∩ Fin ) ⊆ Fin |
| 11 |
10
|
sseli |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin ) |
| 12 |
10
|
sseli |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ Fin ) |
| 13 |
|
unfi |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin ) |
| 14 |
11 12 13
|
syl2an |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin ) |
| 15 |
|
nnunifi |
⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ω ∧ ( 𝐴 ∪ 𝐵 ) ∈ Fin ) → ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω ) |
| 16 |
9 14 15
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω ) |
| 17 |
|
peano2 |
⊢ ( ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω → suc ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω ) |
| 18 |
16 17
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → suc ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω ) |
| 19 |
|
ineq2 |
⊢ ( 𝑎 = ∅ → ( 𝐴 ∩ 𝑎 ) = ( 𝐴 ∩ ∅ ) ) |
| 20 |
19
|
fveq2d |
⊢ ( 𝑎 = ∅ → ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ ∅ ) ) ) |
| 21 |
|
ineq2 |
⊢ ( 𝑎 = ∅ → ( 𝐵 ∩ 𝑎 ) = ( 𝐵 ∩ ∅ ) ) |
| 22 |
21
|
fveq2d |
⊢ ( 𝑎 = ∅ → ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ ∅ ) ) ) |
| 23 |
20 22
|
eqeq12d |
⊢ ( 𝑎 = ∅ → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ ∅ ) ) = ( 𝐹 ‘ ( 𝐵 ∩ ∅ ) ) ) ) |
| 24 |
19 21
|
eqeq12d |
⊢ ( 𝑎 = ∅ → ( ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ↔ ( 𝐴 ∩ ∅ ) = ( 𝐵 ∩ ∅ ) ) ) |
| 25 |
23 24
|
imbi12d |
⊢ ( 𝑎 = ∅ → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ↔ ( ( 𝐹 ‘ ( 𝐴 ∩ ∅ ) ) = ( 𝐹 ‘ ( 𝐵 ∩ ∅ ) ) → ( 𝐴 ∩ ∅ ) = ( 𝐵 ∩ ∅ ) ) ) ) |
| 26 |
25
|
imbi2d |
⊢ ( 𝑎 = ∅ → ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ ∅ ) ) = ( 𝐹 ‘ ( 𝐵 ∩ ∅ ) ) → ( 𝐴 ∩ ∅ ) = ( 𝐵 ∩ ∅ ) ) ) ) ) |
| 27 |
|
ineq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐴 ∩ 𝑎 ) = ( 𝐴 ∩ 𝑏 ) ) |
| 28 |
27
|
fveq2d |
⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) |
| 29 |
|
ineq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐵 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑏 ) ) |
| 30 |
29
|
fveq2d |
⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) |
| 31 |
28 30
|
eqeq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 32 |
27 29
|
eqeq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ↔ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) ) |
| 33 |
31 32
|
imbi12d |
⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ↔ ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 34 |
33
|
imbi2d |
⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) ) ) ) |
| 35 |
|
ineq2 |
⊢ ( 𝑎 = suc 𝑏 → ( 𝐴 ∩ 𝑎 ) = ( 𝐴 ∩ suc 𝑏 ) ) |
| 36 |
35
|
fveq2d |
⊢ ( 𝑎 = suc 𝑏 → ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) ) |
| 37 |
|
ineq2 |
⊢ ( 𝑎 = suc 𝑏 → ( 𝐵 ∩ 𝑎 ) = ( 𝐵 ∩ suc 𝑏 ) ) |
| 38 |
37
|
fveq2d |
⊢ ( 𝑎 = suc 𝑏 → ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 39 |
36 38
|
eqeq12d |
⊢ ( 𝑎 = suc 𝑏 → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ) |
| 40 |
35 37
|
eqeq12d |
⊢ ( 𝑎 = suc 𝑏 → ( ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ↔ ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 41 |
39 40
|
imbi12d |
⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ↔ ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) |
| 42 |
41
|
imbi2d |
⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 43 |
|
ineq2 |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) |
| 44 |
43
|
fveq2d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) |
| 45 |
|
ineq2 |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( 𝐵 ∩ 𝑎 ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) |
| 46 |
45
|
fveq2d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) |
| 47 |
44 46
|
eqeq12d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) ) |
| 48 |
43 45
|
eqeq12d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ↔ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) |
| 49 |
47 48
|
imbi12d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ↔ ( ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) ) |
| 50 |
49
|
imbi2d |
⊢ ( 𝑎 = suc ∪ ( 𝐴 ∪ 𝐵 ) → ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑎 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑎 ) ) → ( 𝐴 ∩ 𝑎 ) = ( 𝐵 ∩ 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) ) ) |
| 51 |
|
in0 |
⊢ ( 𝐴 ∩ ∅ ) = ∅ |
| 52 |
|
in0 |
⊢ ( 𝐵 ∩ ∅ ) = ∅ |
| 53 |
51 52
|
eqtr4i |
⊢ ( 𝐴 ∩ ∅ ) = ( 𝐵 ∩ ∅ ) |
| 54 |
53
|
2a1i |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ ∅ ) ) = ( 𝐹 ‘ ( 𝐵 ∩ ∅ ) ) → ( 𝐴 ∩ ∅ ) = ( 𝐵 ∩ ∅ ) ) ) |
| 55 |
|
simp13 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 56 |
|
3simpa |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ) |
| 57 |
|
ackbij1lem2 |
⊢ ( 𝑏 ∈ 𝐴 → ( 𝐴 ∩ suc 𝑏 ) = ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) |
| 58 |
57
|
fveq2d |
⊢ ( 𝑏 ∈ 𝐴 → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 59 |
58
|
3ad2ant2 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 60 |
|
ackbij1lem4 |
⊢ ( 𝑏 ∈ ω → { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) ) |
| 61 |
60
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) ) |
| 62 |
|
simprl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 63 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 |
| 64 |
1
|
ackbij1lem11 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 ) → ( 𝐴 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 65 |
62 63 64
|
sylancl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐴 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 66 |
|
incom |
⊢ ( { 𝑏 } ∩ ( 𝐴 ∩ 𝑏 ) ) = ( ( 𝐴 ∩ 𝑏 ) ∩ { 𝑏 } ) |
| 67 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝑏 ) ⊆ 𝑏 |
| 68 |
|
nnord |
⊢ ( 𝑏 ∈ ω → Ord 𝑏 ) |
| 69 |
|
orddisj |
⊢ ( Ord 𝑏 → ( 𝑏 ∩ { 𝑏 } ) = ∅ ) |
| 70 |
68 69
|
syl |
⊢ ( 𝑏 ∈ ω → ( 𝑏 ∩ { 𝑏 } ) = ∅ ) |
| 71 |
70
|
adantr |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝑏 ∩ { 𝑏 } ) = ∅ ) |
| 72 |
|
ssdisj |
⊢ ( ( ( 𝐴 ∩ 𝑏 ) ⊆ 𝑏 ∧ ( 𝑏 ∩ { 𝑏 } ) = ∅ ) → ( ( 𝐴 ∩ 𝑏 ) ∩ { 𝑏 } ) = ∅ ) |
| 73 |
67 71 72
|
sylancr |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( ( 𝐴 ∩ 𝑏 ) ∩ { 𝑏 } ) = ∅ ) |
| 74 |
66 73
|
eqtrid |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( { 𝑏 } ∩ ( 𝐴 ∩ 𝑏 ) ) = ∅ ) |
| 75 |
1
|
ackbij1lem9 |
⊢ ( ( { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( { 𝑏 } ∩ ( 𝐴 ∩ 𝑏 ) ) = ∅ ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 76 |
61 65 74 75
|
syl3anc |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 77 |
76
|
3ad2ant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 78 |
59 77
|
eqtrd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 79 |
56 78
|
syl3an1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) ) |
| 80 |
|
ackbij1lem2 |
⊢ ( 𝑏 ∈ 𝐵 → ( 𝐵 ∩ suc 𝑏 ) = ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) |
| 81 |
80
|
fveq2d |
⊢ ( 𝑏 ∈ 𝐵 → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 82 |
81
|
3ad2ant3 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 83 |
|
simprr |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 84 |
|
inss1 |
⊢ ( 𝐵 ∩ 𝑏 ) ⊆ 𝐵 |
| 85 |
1
|
ackbij1lem11 |
⊢ ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∩ 𝑏 ) ⊆ 𝐵 ) → ( 𝐵 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 86 |
83 84 85
|
sylancl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐵 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 87 |
|
incom |
⊢ ( { 𝑏 } ∩ ( 𝐵 ∩ 𝑏 ) ) = ( ( 𝐵 ∩ 𝑏 ) ∩ { 𝑏 } ) |
| 88 |
|
inss2 |
⊢ ( 𝐵 ∩ 𝑏 ) ⊆ 𝑏 |
| 89 |
|
ssdisj |
⊢ ( ( ( 𝐵 ∩ 𝑏 ) ⊆ 𝑏 ∧ ( 𝑏 ∩ { 𝑏 } ) = ∅ ) → ( ( 𝐵 ∩ 𝑏 ) ∩ { 𝑏 } ) = ∅ ) |
| 90 |
88 71 89
|
sylancr |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( ( 𝐵 ∩ 𝑏 ) ∩ { 𝑏 } ) = ∅ ) |
| 91 |
87 90
|
eqtrid |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( { 𝑏 } ∩ ( 𝐵 ∩ 𝑏 ) ) = ∅ ) |
| 92 |
1
|
ackbij1lem9 |
⊢ ( ( { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ ( { 𝑏 } ∩ ( 𝐵 ∩ 𝑏 ) ) = ∅ ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 93 |
61 86 91 92
|
syl3anc |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 94 |
93
|
3ad2ant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 95 |
82 94
|
eqtrd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 96 |
56 95
|
syl3an1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 97 |
55 79 96
|
3eqtr3d |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 98 |
1
|
ackbij1lem10 |
⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω |
| 99 |
98
|
ffvelcdmi |
⊢ ( { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ { 𝑏 } ) ∈ ω ) |
| 100 |
61 99
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐹 ‘ { 𝑏 } ) ∈ ω ) |
| 101 |
98
|
ffvelcdmi |
⊢ ( ( 𝐴 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ∈ ω ) |
| 102 |
65 101
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ∈ ω ) |
| 103 |
98
|
ffvelcdmi |
⊢ ( ( 𝐵 ∩ 𝑏 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ∈ ω ) |
| 104 |
86 103
|
syl |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ∈ ω ) |
| 105 |
|
nnacan |
⊢ ( ( ( 𝐹 ‘ { 𝑏 } ) ∈ ω ∧ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ∈ ω ∧ ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ∈ ω ) → ( ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 106 |
100 102 104 105
|
syl3anc |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ) → ( ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 107 |
106
|
3adant3 |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 108 |
107
|
3ad2ant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 109 |
97 108
|
mpbid |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) |
| 110 |
|
uneq2 |
⊢ ( ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) → ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) = ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) |
| 111 |
110
|
adantl |
⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) = ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) |
| 112 |
57
|
ad2antrr |
⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( { 𝑏 } ∪ ( 𝐴 ∩ 𝑏 ) ) ) |
| 113 |
80
|
ad2antlr |
⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐵 ∩ suc 𝑏 ) = ( { 𝑏 } ∪ ( 𝐵 ∩ 𝑏 ) ) ) |
| 114 |
111 112 113
|
3eqtr4d |
⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) |
| 115 |
114
|
ex |
⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 116 |
115
|
3adant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 117 |
109 116
|
embantd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 118 |
117
|
3exp |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( 𝑏 ∈ 𝐴 → ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 119 |
|
simp13 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 120 |
119
|
eqcomd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) ) |
| 121 |
|
simp12r |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 122 |
|
simp12l |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 123 |
|
simp11 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ω ) |
| 124 |
|
simp3 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 ) |
| 125 |
|
simp2 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝑏 ∈ 𝐴 ) |
| 126 |
1
|
ackbij1lem15 |
⊢ ( ( ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑏 ∈ ω ∧ 𝑏 ∈ 𝐵 ∧ ¬ 𝑏 ∈ 𝐴 ) ) → ¬ ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) ) |
| 127 |
121 122 123 124 125 126
|
syl23anc |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) ) |
| 128 |
120 127
|
pm2.21dd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 129 |
128
|
3exp |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( ¬ 𝑏 ∈ 𝐴 → ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 130 |
118 129
|
pm2.61d |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) |
| 131 |
|
simp13 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 132 |
|
simp12l |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 133 |
|
simp12r |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) |
| 134 |
|
simp11 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ω ) |
| 135 |
|
simp2 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐴 ) |
| 136 |
|
simp3 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ¬ 𝑏 ∈ 𝐵 ) |
| 137 |
1
|
ackbij1lem15 |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑏 ∈ ω ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) ) → ¬ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 138 |
132 133 134 135 136 137
|
syl23anc |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ¬ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 139 |
131 138
|
pm2.21dd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 140 |
139
|
3exp |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( 𝑏 ∈ 𝐴 → ( ¬ 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 141 |
|
simp13 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 142 |
|
ackbij1lem1 |
⊢ ( ¬ 𝑏 ∈ 𝐴 → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐴 ∩ 𝑏 ) ) |
| 143 |
142
|
adantr |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐴 ∩ 𝑏 ) ) |
| 144 |
143
|
fveq2d |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) ) |
| 145 |
|
ackbij1lem1 |
⊢ ( ¬ 𝑏 ∈ 𝐵 → ( 𝐵 ∩ suc 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) |
| 146 |
145
|
adantl |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐵 ∩ suc 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) |
| 147 |
146
|
fveq2d |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) |
| 148 |
144 147
|
eqeq12d |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ↔ ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 149 |
148
|
biimpd |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 150 |
149
|
3adant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) ) |
| 151 |
141 150
|
mpd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) ) |
| 152 |
143 146
|
eqeq12d |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ↔ ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) ) |
| 153 |
152
|
biimprd |
⊢ ( ( ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 154 |
153
|
3adant1 |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 155 |
151 154
|
embantd |
⊢ ( ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) ∧ ¬ 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 156 |
155
|
3exp |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( ¬ 𝑏 ∈ 𝐴 → ( ¬ 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 157 |
140 156
|
pm2.61d |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( ¬ 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) |
| 158 |
130 157
|
pm2.61d |
⊢ ( ( 𝑏 ∈ ω ∧ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) |
| 159 |
158
|
3exp |
⊢ ( 𝑏 ∈ ω → ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 160 |
159
|
com34 |
⊢ ( 𝑏 ∈ ω → ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 161 |
160
|
a2d |
⊢ ( 𝑏 ∈ ω → ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐵 ∩ 𝑏 ) ) ) → ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑏 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑏 ) ) → ( 𝐴 ∩ suc 𝑏 ) = ( 𝐵 ∩ suc 𝑏 ) ) ) ) ) |
| 162 |
26 34 42 50 54 161
|
finds |
⊢ ( suc ∪ ( 𝐴 ∪ 𝐵 ) ∈ ω → ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) ) |
| 163 |
18 162
|
mpcom |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) |
| 164 |
|
omsson |
⊢ ω ⊆ On |
| 165 |
9 164
|
sstrdi |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ On ) |
| 166 |
|
onsucuni |
⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ On → ( 𝐴 ∪ 𝐵 ) ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ) |
| 167 |
165 166
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ) |
| 168 |
167
|
unssad |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐴 ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ) |
| 169 |
|
dfss2 |
⊢ ( 𝐴 ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝐴 ) |
| 170 |
168 169
|
sylib |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝐴 ) |
| 171 |
170
|
fveq2d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ 𝐴 ) ) |
| 172 |
167
|
unssbd |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ) |
| 173 |
|
dfss2 |
⊢ ( 𝐵 ⊆ suc ∪ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝐵 ) |
| 174 |
172 173
|
sylib |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝐵 ) |
| 175 |
174
|
fveq2d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ 𝐵 ) ) |
| 176 |
171 175
|
eqeq12d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ) ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ) ) |
| 177 |
170 174
|
eqeq12d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐴 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐵 ∩ suc ∪ ( 𝐴 ∪ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) ) |
| 178 |
163 176 177
|
3imtr3d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) → 𝐴 = 𝐵 ) ) |