Step | Hyp | Ref
| Expression |
1 | | breq2 4890 |
. . . 4
⊢ (𝑖 = ∅ → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ ∅)) |
2 | 1 | rexbidv 3237 |
. . 3
⊢ (𝑖 = ∅ → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅)) |
3 | | breq2 4890 |
. . . 4
⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎)) |
4 | 3 | rexbidv 3237 |
. . 3
⊢ (𝑖 = 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)) |
5 | | breq2 4890 |
. . . 4
⊢ (𝑖 = suc 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
6 | 5 | rexbidv 3237 |
. . 3
⊢ (𝑖 = suc 𝑎 → (∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
7 | | ordom 7352 |
. . . . 5
⊢ Ord
ω |
8 | | simpl 476 |
. . . . 5
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝑆 ⊆
ω) |
9 | | 0fin 8476 |
. . . . . . . 8
⊢ ∅
∈ Fin |
10 | | eleq1 2847 |
. . . . . . . 8
⊢ (𝑆 = ∅ → (𝑆 ∈ Fin ↔ ∅
∈ Fin)) |
11 | 9, 10 | mpbiri 250 |
. . . . . . 7
⊢ (𝑆 = ∅ → 𝑆 ∈ Fin) |
12 | 11 | necon3bi 2995 |
. . . . . 6
⊢ (¬
𝑆 ∈ Fin → 𝑆 ≠ ∅) |
13 | 12 | adantl 475 |
. . . . 5
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝑆 ≠ ∅) |
14 | | tz7.5 5997 |
. . . . 5
⊢ ((Ord
ω ∧ 𝑆 ⊆
ω ∧ 𝑆 ≠
∅) → ∃𝑗
∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
15 | 7, 8, 13, 14 | mp3an2i 1539 |
. . . 4
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
16 | | en0 8304 |
. . . . . 6
⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑗 ∩ 𝑆) = ∅) |
17 | | incom 4028 |
. . . . . . 7
⊢ (𝑗 ∩ 𝑆) = (𝑆 ∩ 𝑗) |
18 | 17 | eqeq1i 2783 |
. . . . . 6
⊢ ((𝑗 ∩ 𝑆) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅) |
19 | 16, 18 | bitri 267 |
. . . . 5
⊢ ((𝑗 ∩ 𝑆) ≈ ∅ ↔ (𝑆 ∩ 𝑗) = ∅) |
20 | 19 | rexbii 3224 |
. . . 4
⊢
(∃𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ ∅ ↔ ∃𝑗 ∈ 𝑆 (𝑆 ∩ 𝑗) = ∅) |
21 | 15, 20 | sylibr 226 |
. . 3
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ ∅) |
22 | | simplrl 767 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ ω) |
23 | | omsson 7347 |
. . . . . . . . . . 11
⊢ ω
⊆ On |
24 | 22, 23 | syl6ss 3833 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑆 ⊆ On) |
25 | 24 | ssdifssd 3971 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ⊆ On) |
26 | | simplr 759 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ∈ Fin) |
27 | | ssel2 3816 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ ω) |
28 | | onfin2 8440 |
. . . . . . . . . . . . . . . . 17
⊢ ω =
(On ∩ Fin) |
29 | | inss2 4054 |
. . . . . . . . . . . . . . . . 17
⊢ (On ∩
Fin) ⊆ Fin |
30 | 28, 29 | eqsstri 3854 |
. . . . . . . . . . . . . . . 16
⊢ ω
⊆ Fin |
31 | | peano2 7364 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) |
32 | 30, 31 | sseldi 3819 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ω → suc 𝑗 ∈ Fin) |
33 | 27, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ω ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin) |
34 | 33 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → suc 𝑗 ∈ Fin) |
35 | | ssfi 8468 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑗 ∈ Fin ∧ 𝑆 ⊆ suc 𝑗) → 𝑆 ∈ Fin) |
36 | 35 | ex 403 |
. . . . . . . . . . . . 13
⊢ (suc
𝑗 ∈ Fin → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin)) |
37 | 34, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ⊆ suc 𝑗 → 𝑆 ∈ Fin)) |
38 | 26, 37 | mtod 190 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → ¬ 𝑆 ⊆ suc 𝑗) |
39 | | ssdif0 4172 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) = ∅) |
40 | 39 | necon3bbii 3016 |
. . . . . . . . . . 11
⊢ (¬
𝑆 ⊆ suc 𝑗 ↔ (𝑆 ∖ suc 𝑗) ≠ ∅) |
41 | 38, 40 | sylib 210 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑗 ∈ 𝑆) → (𝑆 ∖ suc 𝑗) ≠ ∅) |
42 | 41 | ad2ant2lr 738 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑆 ∖ suc 𝑗) ≠ ∅) |
43 | | onint 7273 |
. . . . . . . . 9
⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ (𝑆 ∖ suc 𝑗) ≠ ∅) → ∩ (𝑆
∖ suc 𝑗) ∈
(𝑆 ∖ suc 𝑗)) |
44 | 25, 42, 43 | syl2anc 579 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ (𝑆 ∖ suc 𝑗)) |
45 | 44 | eldifad 3804 |
. . . . . . 7
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∩ (𝑆 ∖ suc 𝑗) ∈ 𝑆) |
46 | | simprr 763 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑗 ∩ 𝑆) ≈ 𝑎) |
47 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
48 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
49 | | en2sn 8325 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ V ∧ 𝑎 ∈ V) → {𝑗} ≈ {𝑎}) |
50 | 47, 48, 49 | mp2an 682 |
. . . . . . . . . 10
⊢ {𝑗} ≈ {𝑎} |
51 | 50 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → {𝑗} ≈ {𝑎}) |
52 | | simprl 761 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ 𝑆) |
53 | 22, 52 | sseldd 3822 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → 𝑗 ∈ ω) |
54 | | nnord 7351 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → Ord 𝑗) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord 𝑗) |
56 | | ordirr 5994 |
. . . . . . . . . . . 12
⊢ (Ord
𝑗 → ¬ 𝑗 ∈ 𝑗) |
57 | | elinel1 4022 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝑗 ∩ 𝑆) → 𝑗 ∈ 𝑗) |
58 | 56, 57 | nsyl 138 |
. . . . . . . . . . 11
⊢ (Ord
𝑗 → ¬ 𝑗 ∈ (𝑗 ∩ 𝑆)) |
59 | | disjsn 4478 |
. . . . . . . . . . 11
⊢ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ↔ ¬ 𝑗 ∈ (𝑗 ∩ 𝑆)) |
60 | 58, 59 | sylibr 226 |
. . . . . . . . . 10
⊢ (Ord
𝑗 → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅) |
61 | 55, 60 | syl 17 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅) |
62 | | nnord 7351 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ω → Ord 𝑎) |
63 | | ordirr 5994 |
. . . . . . . . . . . 12
⊢ (Ord
𝑎 → ¬ 𝑎 ∈ 𝑎) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ω → ¬
𝑎 ∈ 𝑎) |
65 | | disjsn 4478 |
. . . . . . . . . . 11
⊢ ((𝑎 ∩ {𝑎}) = ∅ ↔ ¬ 𝑎 ∈ 𝑎) |
66 | 64, 65 | sylibr 226 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ω → (𝑎 ∩ {𝑎}) = ∅) |
67 | 66 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑎 ∩ {𝑎}) = ∅) |
68 | | unen 8328 |
. . . . . . . . 9
⊢ ((((𝑗 ∩ 𝑆) ≈ 𝑎 ∧ {𝑗} ≈ {𝑎}) ∧ (((𝑗 ∩ 𝑆) ∩ {𝑗}) = ∅ ∧ (𝑎 ∩ {𝑎}) = ∅)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎})) |
69 | 46, 51, 61, 67, 68 | syl22anc 829 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ {𝑗}) ≈ (𝑎 ∪ {𝑎})) |
70 | | simprr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑏 ∈ 𝑆) |
71 | | simplrl 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ ω) |
72 | 71, 23 | syl6ss 3833 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → 𝑆 ⊆ On) |
73 | | ordsuc 7292 |
. . . . . . . . . . . . . . . . . 18
⊢ (Ord
𝑗 ↔ Ord suc 𝑗) |
74 | 55, 73 | sylib 210 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → Ord suc 𝑗) |
75 | 74 | adantrr 707 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → Ord suc 𝑗) |
76 | | simp2 1128 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → 𝑆 ⊆ On) |
77 | 76 | ssdifssd 3971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ On) |
78 | | simpl1 1199 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ 𝑆) |
79 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → ¬ 𝑏 ∈ suc 𝑗) |
80 | 78, 79 | eldifd 3803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ ¬ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ (𝑆 ∖ suc 𝑗)) |
81 | 80 | ex 403 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → 𝑏 ∈ (𝑆 ∖ suc 𝑗))) |
82 | | onnmin 7281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∖ suc 𝑗) ⊆ On ∧ 𝑏 ∈ (𝑆 ∖ suc 𝑗)) → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) |
83 | 77, 81, 82 | syl6an 674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (¬ 𝑏 ∈ suc 𝑗 → ¬ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗))) |
84 | 83 | con4d 115 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) → 𝑏 ∈ suc 𝑗)) |
85 | 84 | imp 397 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) → 𝑏 ∈ suc 𝑗) |
86 | | simp3 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → Ord suc 𝑗) |
87 | | ordsucss 7296 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Ord suc
𝑗 → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ suc 𝑗 → suc 𝑏 ⊆ suc 𝑗)) |
89 | 88 | imp 397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → suc 𝑏 ⊆ suc 𝑗) |
90 | 89 | sscond 3970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → (𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏)) |
91 | | intss 4731 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∖ suc 𝑗) ⊆ (𝑆 ∖ suc 𝑏) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → ∩ (𝑆 ∖ suc 𝑏) ⊆ ∩ (𝑆 ∖ suc 𝑗)) |
93 | | simpl2 1201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑆 ⊆ On) |
94 | | ordelon 6000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Ord suc
𝑗 ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On) |
95 | 86, 94 | sylan 575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ On) |
96 | | onmindif 6065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ On ∧ 𝑏 ∈ On) → 𝑏 ∈ ∩ (𝑆
∖ suc 𝑏)) |
97 | 93, 95, 96 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑏)) |
98 | 92, 97 | sseldd 3822 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) ∧ 𝑏 ∈ suc 𝑗) → 𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗)) |
99 | 85, 98 | impbida 791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ 𝑆 ∧ 𝑆 ⊆ On ∧ Ord suc 𝑗) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗)) |
100 | 70, 72, 75, 99 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ suc 𝑗)) |
101 | | df-suc 5982 |
. . . . . . . . . . . . . . . 16
⊢ suc 𝑗 = (𝑗 ∪ {𝑗}) |
102 | 101 | eleq2i 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ suc 𝑗 ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})) |
103 | 100, 102 | syl6bb 279 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧
((𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎) ∧ 𝑏 ∈ 𝑆)) → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗}))) |
104 | 103 | expr 450 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ 𝑆 → (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ↔ 𝑏 ∈ (𝑗 ∪ {𝑗})))) |
105 | 104 | pm5.32rd 573 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆))) |
106 | | elin 4019 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (∩ (𝑆
∖ suc 𝑗) ∩ 𝑆) ↔ (𝑏 ∈ ∩ (𝑆 ∖ suc 𝑗) ∧ 𝑏 ∈ 𝑆)) |
107 | | elin 4019 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆) ↔ (𝑏 ∈ (𝑗 ∪ {𝑗}) ∧ 𝑏 ∈ 𝑆)) |
108 | 105, 106,
107 | 3bitr4g 306 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (𝑏 ∈ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ↔ 𝑏 ∈ ((𝑗 ∪ {𝑗}) ∩ 𝑆))) |
109 | 108 | eqrdv 2776 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∪ {𝑗}) ∩ 𝑆)) |
110 | | indir 4102 |
. . . . . . . . . 10
⊢ ((𝑗 ∪ {𝑗}) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) |
111 | 109, 110 | syl6eq 2830 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆))) |
112 | | snssi 4570 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝑆 → {𝑗} ⊆ 𝑆) |
113 | | df-ss 3806 |
. . . . . . . . . . . 12
⊢ ({𝑗} ⊆ 𝑆 ↔ ({𝑗} ∩ 𝑆) = {𝑗}) |
114 | 112, 113 | sylib 210 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑆 → ({𝑗} ∩ 𝑆) = {𝑗}) |
115 | 114 | uneq2d 3990 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑆 → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
116 | 115 | ad2antrl 718 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ((𝑗 ∩ 𝑆) ∪ ({𝑗} ∩ 𝑆)) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
117 | 111, 116 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) = ((𝑗 ∩ 𝑆) ∪ {𝑗})) |
118 | | df-suc 5982 |
. . . . . . . . 9
⊢ suc 𝑎 = (𝑎 ∪ {𝑎}) |
119 | 118 | a1i 11 |
. . . . . . . 8
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → suc 𝑎 = (𝑎 ∪ {𝑎})) |
120 | 69, 117, 119 | 3brtr4d 4918 |
. . . . . . 7
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → (∩
(𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) |
121 | | ineq1 4030 |
. . . . . . . . 9
⊢ (𝑏 = ∩
(𝑆 ∖ suc 𝑗) → (𝑏 ∩ 𝑆) = (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆)) |
122 | 121 | breq1d 4896 |
. . . . . . . 8
⊢ (𝑏 = ∩
(𝑆 ∖ suc 𝑗) → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (∩ (𝑆 ∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎)) |
123 | 122 | rspcev 3511 |
. . . . . . 7
⊢ ((∩ (𝑆
∖ suc 𝑗) ∈ 𝑆 ∧ (∩ (𝑆
∖ suc 𝑗) ∩ 𝑆) ≈ suc 𝑎) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎) |
124 | 45, 120, 123 | syl2anc 579 |
. . . . . 6
⊢ (((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) ∧ (𝑗 ∈ 𝑆 ∧ (𝑗 ∩ 𝑆) ≈ 𝑎)) → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎) |
125 | 124 | rexlimdvaa 3214 |
. . . . 5
⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑏 ∈ 𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎)) |
126 | | ineq1 4030 |
. . . . . . 7
⊢ (𝑏 = 𝑗 → (𝑏 ∩ 𝑆) = (𝑗 ∩ 𝑆)) |
127 | 126 | breq1d 4896 |
. . . . . 6
⊢ (𝑏 = 𝑗 → ((𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
128 | 127 | cbvrexv 3368 |
. . . . 5
⊢
(∃𝑏 ∈
𝑆 (𝑏 ∩ 𝑆) ≈ suc 𝑎 ↔ ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎) |
129 | 125, 128 | syl6ib 243 |
. . . 4
⊢ ((𝑎 ∈ ω ∧ (𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin)) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎)) |
130 | 129 | ex 403 |
. . 3
⊢ (𝑎 ∈ ω → ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
(∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ suc 𝑎))) |
131 | 2, 4, 6, 21, 130 | finds2 7372 |
. 2
⊢ (𝑖 ∈ ω → ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) |
132 | 131 | impcom 398 |
1
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) →
∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) |