Step | Hyp | Ref
| Expression |
1 | | cofon2.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝒫 On) |
2 | | cofon2.3 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
3 | | sseq1 3970 |
. . . . . . . 8
⊢ (𝑧 = 𝑏 → (𝑧 ⊆ 𝑤 ↔ 𝑏 ⊆ 𝑤)) |
4 | 3 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤)) |
5 | | cofon2.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
6 | 5 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
7 | | simpr 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
8 | 4, 6, 7 | rspcdva 3583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑤 ∈ 𝐴 𝑏 ⊆ 𝑤) |
9 | | sseq2 3971 |
. . . . . . 7
⊢ (𝑤 = 𝑐 → (𝑏 ⊆ 𝑤 ↔ 𝑏 ⊆ 𝑐)) |
10 | 9 | cbvrexvw 3227 |
. . . . . 6
⊢
(∃𝑤 ∈
𝐴 𝑏 ⊆ 𝑤 ↔ ∃𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐) |
11 | 8, 10 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐) |
12 | | ssintub 4928 |
. . . . . . . . 9
⊢ 𝐴 ⊆ ∩ {𝑎
∈ On ∣ 𝐴 ⊆
𝑎} |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) |
14 | 13 | sselda 3945 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) |
15 | | cofon2.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝒫 On) |
16 | 15 | elpwid 4570 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ On) |
17 | 16 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → 𝐵 ⊆ On) |
18 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
19 | 17, 18 | sseldd 3946 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → 𝑏 ∈ On) |
20 | 1 | elpwid 4570 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ On) |
21 | | ssorduni 7714 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Ord ∪ 𝐴) |
23 | | ordsuc 7749 |
. . . . . . . . . . . . 13
⊢ (Ord
∪ 𝐴 ↔ Ord suc ∪
𝐴) |
24 | 22, 23 | sylib 217 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord suc ∪ 𝐴) |
25 | 1 | uniexd 7680 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝐴
∈ V) |
26 | | sucexg 7741 |
. . . . . . . . . . . . 13
⊢ (∪ 𝐴
∈ V → suc ∪ 𝐴 ∈ V) |
27 | | elong 6326 |
. . . . . . . . . . . . 13
⊢ (suc
∪ 𝐴 ∈ V → (suc ∪ 𝐴
∈ On ↔ Ord suc ∪ 𝐴)) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (suc ∪ 𝐴
∈ On ↔ Ord suc ∪ 𝐴)) |
29 | 24, 28 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → suc ∪ 𝐴
∈ On) |
30 | | onsucuni 7764 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) |
31 | 20, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ suc ∪
𝐴) |
32 | | sseq2 3971 |
. . . . . . . . . . . 12
⊢ (𝑎 = suc ∪ 𝐴
→ (𝐴 ⊆ 𝑎 ↔ 𝐴 ⊆ suc ∪
𝐴)) |
33 | 32 | rspcev 3582 |
. . . . . . . . . . 11
⊢ ((suc
∪ 𝐴 ∈ On ∧ 𝐴 ⊆ suc ∪
𝐴) → ∃𝑎 ∈ On 𝐴 ⊆ 𝑎) |
34 | 29, 31, 33 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → ∃𝑎 ∈ On 𝐴 ⊆ 𝑎) |
35 | | onintrab2 7733 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈ On
𝐴 ⊆ 𝑎 ↔ ∩ {𝑎
∈ On ∣ 𝐴 ⊆
𝑎} ∈
On) |
36 | 34, 35 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → ∩ {𝑎
∈ On ∣ 𝐴 ⊆
𝑎} ∈
On) |
37 | 36 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎} ∈ On) |
38 | | ontr2 6365 |
. . . . . . . 8
⊢ ((𝑏 ∈ On ∧ ∩ {𝑎
∈ On ∣ 𝐴 ⊆
𝑎} ∈ On) →
((𝑏 ⊆ 𝑐 ∧ 𝑐 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎})) |
39 | 19, 37, 38 | syl2anc 585 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → ((𝑏 ⊆ 𝑐 ∧ 𝑐 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎})) |
40 | 14, 39 | mpan2d 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐴) → (𝑏 ⊆ 𝑐 → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎})) |
41 | 40 | rexlimdva 3153 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 𝑏 ⊆ 𝑐 → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎})) |
42 | 11, 41 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) |
43 | 42 | ex 414 |
. . 3
⊢ (𝜑 → (𝑏 ∈ 𝐵 → 𝑏 ∈ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎})) |
44 | 43 | ssrdv 3951 |
. 2
⊢ (𝜑 → 𝐵 ⊆ ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎}) |
45 | 1, 2, 44 | cofon1 8619 |
1
⊢ (𝜑 → ∩ {𝑎
∈ On ∣ 𝐴 ⊆
𝑎} = ∩ {𝑏
∈ On ∣ 𝐵 ⊆
𝑏}) |