Proof of Theorem isf32lem7
Step | Hyp | Ref
| Expression |
1 | | isf32lem.f |
. . . . 5
⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) |
2 | 1 | fveq1i 6104 |
. . . 4
⊢ (𝐾‘𝐴) = (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) |
3 | | isf32lem.d |
. . . . . . . . . 10
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
4 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ⊆ ω |
5 | 3, 4 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ω |
6 | | isf32lem.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
7 | | isf32lem.b |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
8 | | isf32lem.c |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
9 | 6, 7, 8, 3 | isf32lem5 9062 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑆 ∈ Fin) |
10 | | isf32lem.e |
. . . . . . . . . 10
⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) |
11 | 10 | fin23lem22 9032 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐽:ω–1-1-onto→𝑆) |
12 | 5, 9, 11 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:ω–1-1-onto→𝑆) |
13 | | f1of 6050 |
. . . . . . . 8
⊢ (𝐽:ω–1-1-onto→𝑆 → 𝐽:ω⟶𝑆) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽:ω⟶𝑆) |
15 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
16 | 14, 15 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
17 | 16 | ad2ant2r 779 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
18 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐽:ω⟶𝑆) |
19 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ∈
ω) |
20 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐴 ∈ ω) → (𝐽‘𝐴) ∈ 𝑆) |
21 | 18, 19, 20 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ∈ 𝑆) |
22 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘𝑤) = (𝐹‘(𝐽‘𝐴))) |
23 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑤 = (𝐽‘𝐴) → suc 𝑤 = suc (𝐽‘𝐴)) |
24 | 23 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘suc 𝑤) = (𝐹‘suc (𝐽‘𝐴))) |
25 | 22, 24 | difeq12d 3691 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐴) → ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
26 | | eqid 2610 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) = (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) |
27 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(𝐽‘𝐴)) ∈ V |
28 | | difexg 4735 |
. . . . . . . 8
⊢ ((𝐹‘(𝐽‘𝐴)) ∈ V → ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∈ V) |
29 | 27, 28 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∈ V |
30 | 25, 26, 29 | fvmpt 6191 |
. . . . . 6
⊢ ((𝐽‘𝐴) ∈ 𝑆 → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
31 | 21, 30 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
32 | 17, 31 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
33 | 2, 32 | syl5eq 2656 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐾‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
34 | 1 | fveq1i 6104 |
. . . 4
⊢ (𝐾‘𝐵) = (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) |
35 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐵 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
36 | 14, 35 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
37 | 36 | ad2ant2rl 781 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵))) |
38 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ∈
ω) |
39 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐵 ∈ ω) → (𝐽‘𝐵) ∈ 𝑆) |
40 | 18, 38, 39 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐵) ∈ 𝑆) |
41 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐵) → (𝐹‘𝑤) = (𝐹‘(𝐽‘𝐵))) |
42 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑤 = (𝐽‘𝐵) → suc 𝑤 = suc (𝐽‘𝐵)) |
43 | 42 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐵) → (𝐹‘suc 𝑤) = (𝐹‘suc (𝐽‘𝐵))) |
44 | 41, 43 | difeq12d 3691 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐵) → ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
45 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(𝐽‘𝐵)) ∈ V |
46 | | difexg 4735 |
. . . . . . . 8
⊢ ((𝐹‘(𝐽‘𝐵)) ∈ V → ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵))) ∈ V) |
47 | 45, 46 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵))) ∈ V |
48 | 44, 26, 47 | fvmpt 6191 |
. . . . . 6
⊢ ((𝐽‘𝐵) ∈ 𝑆 → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
49 | 40, 48 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐵)) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
50 | 37, 49 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐵) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
51 | 34, 50 | syl5eq 2656 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐾‘𝐵) = ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) |
52 | 33, 51 | ineq12d 3777 |
. 2
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵))))) |
53 | | simpll 786 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → 𝜑) |
54 | | simplr 788 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → 𝐴 ≠ 𝐵) |
55 | | f1of1 6049 |
. . . . . . . . 9
⊢ (𝐽:ω–1-1-onto→𝑆 → 𝐽:ω–1-1→𝑆) |
56 | 12, 55 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽:ω–1-1→𝑆) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐽:ω–1-1→𝑆) |
58 | | f1fveq 6420 |
. . . . . . 7
⊢ ((𝐽:ω–1-1→𝑆 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) ↔ 𝐴 = 𝐵)) |
59 | 57, 58 | sylan 487 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) ↔ 𝐴 = 𝐵)) |
60 | 59 | biimpd 218 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐽‘𝐴) = (𝐽‘𝐵) → 𝐴 = 𝐵)) |
61 | 60 | necon3d 2803 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ≠ 𝐵 → (𝐽‘𝐴) ≠ (𝐽‘𝐵))) |
62 | 54, 61 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ≠ (𝐽‘𝐵)) |
63 | 5, 21 | sseldi 3566 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐴) ∈ ω) |
64 | 5, 40 | sseldi 3566 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐽‘𝐵) ∈ ω) |
65 | 6, 7, 8 | isf32lem4 9061 |
. . 3
⊢ (((𝜑 ∧ (𝐽‘𝐴) ≠ (𝐽‘𝐵)) ∧ ((𝐽‘𝐴) ∈ ω ∧ (𝐽‘𝐵) ∈ ω)) → (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) = ∅) |
66 | 53, 62, 63, 64, 65 | syl22anc 1319 |
. 2
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∩ ((𝐹‘(𝐽‘𝐵)) ∖ (𝐹‘suc (𝐽‘𝐵)))) = ∅) |
67 | 52, 66 | eqtrd 2644 |
1
⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = ∅) |