Proof of Theorem isf32lem7
Step | Hyp | Ref
| Expression |
1 | | isf32lem.f |
. . . . 5
⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) |
2 | 1 | fveq1i 6772 |
. . . 4
⊢ (𝐾‘𝐴) = (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) |
3 | | isf32lem.d |
. . . . . . . . . 10
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
4 | 3 | ssrab3 4020 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ω |
5 | | isf32lem.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
6 | | isf32lem.b |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
7 | | isf32lem.c |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
8 | 5, 6, 7, 3 | isf32lem5 10114 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑆 ∈ Fin) |
9 | | isf32lem.e |
. . . . . . . . . 10
⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) |
10 | 9 | fin23lem22 10084 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐽:ω–1-1-onto→𝑆) |
11 | 4, 8, 10 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:ω–1-1-onto→𝑆) |
12 | | f1of 6714 |
. . . . . . . 8
⊢ (𝐽:ω–1-1-onto→𝑆 → 𝐽:ω⟶𝑆) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽:ω⟶𝑆) |
14 | | fvco3 6864 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
15 | 13, 14 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
16 | 15 | ad2ant2r 744 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
17 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐽:ω⟶𝑆) |
18 | | simpl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ∈
ω) |
19 | | ffvelrn 6956 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐴 ∈ ω) → (𝐽‘𝐴) ∈ 𝑆) |
20 | 17, 18, 19 | syl2an 596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ∈ 𝑆) |
21 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘𝑤) = (𝐹‘(𝐽‘𝐴))) |
22 | | suceq 6330 |
. . . . . . . . 9
⊢ (𝑤 = (𝐽‘𝐴) → suc 𝑤 = suc (𝐽‘𝐴)) |
23 | 22 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘suc 𝑤) = (𝐹‘suc (𝐽‘𝐴))) |
24 | 21, 23 | difeq12d 4063 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐴) → ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
25 | | eqid 2740 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) = (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) |
26 | | fvex 6784 |
. . . . . . . 8
⊢ (𝐹‘(𝐽‘𝐴)) ∈ V |
27 | 26 | difexi 5256 |
. . . . . . 7
⊢ ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∈ V |
28 | 24, 25, 27 | fvmpt 6872 |
. . . . . 6
⊢ ((𝐽‘𝐴) ∈ 𝑆 → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
29 | 20, 28 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
30 | 16, 29 | eqtrd 2780 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
31 | 2, 30 | eqtrid 2792 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐾‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
32 | 1 | fveq1i 6772 |
. . . 4
⊢ (𝐾‘𝐵) = (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) |
33 | | fvco3 6864 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐵 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
34 | 13, 33 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
35 | 34 | ad2ant2rl 746 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
36 | | simpr 485 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ∈
ω) |
37 | | ffvelrn 6956 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐵 ∈ ω) → (𝐽‘𝐵) ∈ 𝑆) |
38 | 17, 36, 37 | syl2an 596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐵) ∈ 𝑆) |
39 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐵) → (𝐹‘𝑤) = (𝐹‘(𝐽‘𝐵))) |
40 | | suceq 6330 |
. . . . . . . . 9
⊢ (𝑤 = (𝐽‘𝐵) → suc 𝑤 = suc (𝐽‘𝐵)) |
41 | 40 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐵) → (𝐹‘suc 𝑤) = (𝐹‘suc (𝐽‘𝐵))) |
42 | 39, 41 | difeq12d 4063 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐵) → ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
43 | | fvex 6784 |
. . . . . . . 8
⊢ (𝐹‘(𝐽‘𝐵)) ∈ V |
44 | 43 | difexi 5256 |
. . . . . . 7
⊢ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵))) ∈ V |
45 | 42, 25, 44 | fvmpt 6872 |
. . . . . 6
⊢ ((𝐽‘𝐵) ∈ 𝑆 → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
46 | 38, 45 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
47 | 35, 46 | eqtrd 2780 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
48 | 32, 47 | eqtrid 2792 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐾‘𝐵) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
49 | 31, 48 | ineq12d 4153 |
. 2
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵))))) |
50 | | simpll 764 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → 𝜑) |
51 | | simplr 766 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → 𝐴 ≠ 𝐵) |
52 | | f1of1 6713 |
. . . . . . . . 9
⊢ (𝐽:ω–1-1-onto→𝑆 → 𝐽:ω–1-1→𝑆) |
53 | 11, 52 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:ω–1-1→𝑆) |
54 | 53 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐽:ω–1-1→𝑆) |
55 | | f1fveq 7132 |
. . . . . . 7
⊢ ((𝐽:ω–1-1→𝑆 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) ↔ 𝐴 = 𝐵)) |
56 | 54, 55 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) ↔ 𝐴 = 𝐵)) |
57 | 56 | biimpd 228 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) → 𝐴 = 𝐵)) |
58 | 57 | necon3d 2966 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ≠ 𝐵 → (𝐽‘𝐴) ≠ (𝐽‘𝐵))) |
59 | 51, 58 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ≠ (𝐽‘𝐵)) |
60 | 4, 20 | sselid 3924 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ∈ ω) |
61 | 4, 38 | sselid 3924 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐵) ∈ ω) |
62 | 5, 6, 7 | isf32lem4 10113 |
. . 3
⊢ (((𝜑 ∧ (𝐽‘𝐴) ≠ (𝐽‘𝐵)) ∧ ((𝐽‘𝐴) ∈ ω ∧ (𝐽‘𝐵) ∈ ω)) → (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) = ∅) |
63 | 50, 59, 60, 61, 62 | syl22anc 836 |
. 2
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) = ∅) |
64 | 49, 63 | eqtrd 2780 |
1
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = ∅) |