Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. . . 4
⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅)) |
2 | 1 | rexbidv 3052 |
. . 3
⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)) |
3 | | breq2 4657 |
. . . 4
⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎)) |
4 | 3 | rexbidv 3052 |
. . 3
⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)) |
5 | | breq2 4657 |
. . . 4
⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
6 | 5 | rexbidv 3052 |
. . 3
⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
7 | | ordom 7074 |
. . . . . 6
⊢ Ord
ω |
8 | 7 | a1i 11 |
. . . . 5
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → Ord
ω) |
9 | | simpl 473 |
. . . . 5
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝑆 ⊆
ω) |
10 | | 0fin 8188 |
. . . . . . . 8
⊢ ∅
∈ Fin |
11 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅
∈ Fin)) |
12 | 10, 11 | mpbiri 248 |
. . . . . . 7
⊢ (𝑆 = ∅ → 𝑆 ∈ Fin) |
13 | 12 | necon3bi 2820 |
. . . . . 6
⊢ (¬
𝑆 ∈ Fin → 𝑆 ≠ ∅) |
14 | 13 | adantl 482 |
. . . . 5
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝑆 ≠ ∅) |
15 | | tz7.5 5744 |
. . . . 5
⊢ ((Ord
ω ∧ 𝑆 ⊆
ω ∧ 𝑆 ≠
∅) → ∃𝑗
∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
16 | 8, 9, 14, 15 | syl3anc 1326 |
. . . 4
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
17 | | en0 8019 |
. . . . . 6
⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅) |
18 | | incom 3805 |
. . . . . . 7
⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗) |
19 | 18 | eqeq1i 2627 |
. . . . . 6
⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅) |
20 | 17, 19 | bitri 264 |
. . . . 5
⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅) |
21 | 20 | rexbii 3041 |
. . . 4
⊢
(∃𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
22 | 16, 21 | sylibr 224 |
. . 3
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅) |
23 | | simplrl 800 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω) |
24 | | omsson 7069 |
. . . . . . . . . . 11
⊢ ω
⊆ On |
25 | 23, 24 | syl6ss 3615 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On) |
26 | 25 | ssdifssd 3748 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On) |
27 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin) |
28 | | ssel2 3598 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω) |
29 | | onfin2 8152 |
. . . . . . . . . . . . . . . . 17
⊢ ω =
(On ∩ Fin) |
30 | | inss2 3834 |
. . . . . . . . . . . . . . . . 17
⊢ (On ∩
Fin) ⊆ Fin |
31 | 29, 30 | eqsstri 3635 |
. . . . . . . . . . . . . . . 16
⊢ ω
⊆ Fin |
32 | | peano2 7086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) |
33 | 31, 32 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin) |
34 | 28, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin) |
35 | 34 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin) |
36 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin) |
37 | 36 | ex 450 |
. . . . . . . . . . . . 13
⊢ (suc
𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin)) |
38 | 35, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin)) |
39 | 27, 38 | mtod 189 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗) |
40 | | ssdif0 3942 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅) |
41 | 40 | necon3bbii 2841 |
. . . . . . . . . . 11
⊢ (¬
𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅) |
42 | 39, 41 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅) |
43 | 42 | ad2ant2lr 784 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅) |
44 | | onint 6995 |
. . . . . . . . 9
⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆
∖ suc 𝑗) ∈
(𝑆 ∖ suc 𝑗)) |
45 | 26, 43, 44 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗)) |
46 | 45 | eldifad 3586 |
. . . . . . 7
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆) |
47 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎) |
48 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
49 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
50 | | en2sn 8037 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎}) |
51 | 48, 49, 50 | mp2an 708 |
. . . . . . . . . 10
⊢ {𝑗} ≈ {𝑎} |
52 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎}) |
53 | | simprl 794 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆) |
54 | 23, 53 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω) |
55 | | nnord 7073 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → Ord 𝑗) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗) |
57 | | ordirr 5741 |
. . . . . . . . . . . 12
⊢ (Ord
𝑗 → ¬ 𝑗 ∈ 𝑗) |
58 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∩ 𝑆) ⊆ 𝑗 |
59 | 58 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗) |
60 | 57, 59 | nsyl 135 |
. . . . . . . . . . 11
⊢ (Ord
𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆)) |
61 | | disjsn 4246 |
. . . . . . . . . . 11
⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆)) |
62 | 60, 61 | sylibr 224 |
. . . . . . . . . 10
⊢ (Ord
𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅) |
63 | 56, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅) |
64 | | nnord 7073 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ω → Ord 𝑎) |
65 | | ordirr 5741 |
. . . . . . . . . . . 12
⊢ (Ord
𝑎 → ¬ 𝑎 ∈ 𝑎) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω → ¬
𝑎 ∈ 𝑎) |
67 | | disjsn 4246 |
. . . . . . . . . . 11
⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎) |
68 | 66, 67 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅) |
69 | 68 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅) |
70 | | unen 8040 |
. . . . . . . . 9
⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎})) |
71 | 47, 52, 63, 69, 70 | syl22anc 1327 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎})) |
72 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆) |
73 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω) |
74 | 73, 24 | syl6ss 3615 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On) |
75 | | ordsuc 7014 |
. . . . . . . . . . . . . . . . . 18
⊢ (Ord
𝑗 ↔ Ord suc 𝑗) |
76 | 56, 75 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗) |
77 | 76 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗) |
78 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On) |
79 | 78 | ssdifssd 3748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On) |
80 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆) |
81 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗) |
82 | 80, 81 | eldifd 3585 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗)) |
83 | 82 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗))) |
84 | | onnmin 7003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) |
85 | 79, 83, 84 | syl6an 568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))) |
86 | 85 | con4d 114 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗)) |
87 | 86 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗) |
88 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗) |
89 | | ordsucss 7018 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Ord suc
𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗)) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗)) |
91 | 90 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗) |
92 | 91 | sscond 3747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏)) |
93 | | intss 4498 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗)) |
95 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On) |
96 | | ordelon 5747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord suc
𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On) |
97 | 88, 96 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On) |
98 | | onmindif 5815 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆
∖ suc 𝑏)) |
99 | 95, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏)) |
100 | 94, 99 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) |
101 | 87, 100 | impbida 877 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗)) |
102 | 72, 74, 77, 101 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗)) |
103 | | df-suc 5729 |
. . . . . . . . . . . . . . . 16
⊢ suc 𝑗 = (𝑗 ∪ {𝑗}) |
104 | 103 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})) |
105 | 102, 104 | syl6bb 276 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))) |
106 | 105 | expr 643 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))) |
107 | 106 | pm5.32rd 672 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))) |
108 | | elin 3796 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (∩ (𝑆
∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆)) |
109 | | elin 3796 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)) |
110 | 107, 108,
109 | 3bitr4g 303 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆))) |
111 | 110 | eqrdv 2620 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆)) |
112 | | indir 3875 |
. . . . . . . . . 10
⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) |
113 | 111, 112 | syl6eq 2672 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))) |
114 | | snssi 4339 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆) |
115 | | df-ss 3588 |
. . . . . . . . . . . 12
⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗}) |
116 | 114, 115 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗}) |
117 | 116 | uneq2d 3767 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
118 | 117 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
119 | 113, 118 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
120 | | df-suc 5729 |
. . . . . . . . 9
⊢ suc 𝑎 = (𝑎 ∪ {𝑎}) |
121 | 120 | a1i 11 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎})) |
122 | 71, 119, 121 | 3brtr4d 4685 |
. . . . . . 7
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) |
123 | | ineq1 3807 |
. . . . . . . . 9
⊢ (𝑏 = ∩
(𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆)) |
124 | 123 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑏 = ∩
(𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)) |
125 | 124 | rspcev 3309 |
. . . . . . 7
⊢ ((∩ (𝑆
∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆
∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎) |
126 | 46, 122, 125 | syl2anc 693 |
. . . . . 6
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎) |
127 | 126 | rexlimdvaa 3032 |
. . . . 5
⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)) |
128 | | ineq1 3807 |
. . . . . . 7
⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆)) |
129 | 128 | breq1d 4663 |
. . . . . 6
⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
130 | 129 | cbvrexv 3172 |
. . . . 5
⊢
(∃𝑏 ∈
𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎) |
131 | 127, 130 | syl6ib 241 |
. . . 4
⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
132 | 131 | ex 450 |
. . 3
⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))) |
133 | 2, 4, 6, 22, 132 | finds2 7094 |
. 2
⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) |
134 | 133 | impcom 446 |
1
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) |