Step | Hyp | Ref
| Expression |
1 | | sseq2 3971 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ 𝑧)) |
2 | 1 | cbvrabv 3418 |
. . . 4
⊢ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} = {𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧} |
3 | | sseq1 3970 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) |
4 | 3 | rexbidv 3176 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦)) |
5 | | cofon1.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
7 | | simprr 772 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝑎 ∈ 𝐴) |
8 | 4, 6, 7 | rspcdva 3583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦) |
9 | | sseq2 3971 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → (𝑎 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑏)) |
10 | 9 | cbvrexvw 3227 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐵 𝑎 ⊆ 𝑦 ↔ ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
11 | 8, 10 | sylib 217 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
12 | | simprl 770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝐵 ⊆ 𝑧) |
13 | 12 | sselda 3945 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑧) |
14 | | cofon1.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ 𝒫 On) |
15 | 14 | elpwid 4570 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ On) |
16 | 15 | ad3antrrr 729 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ On) |
17 | | simplrr 777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐴) |
18 | 16, 17 | sseldd 3946 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ On) |
19 | | simpllr 775 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑧 ∈ On) |
20 | | ontr2 6365 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ On) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧) → 𝑎 ∈ 𝑧)) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧) → 𝑎 ∈ 𝑧)) |
22 | 13, 21 | mpan2d 693 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → (𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧)) |
23 | 22 | rexlimdva 3153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧)) |
24 | 11, 23 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝑎 ∈ 𝑧) |
25 | 24 | expr 458 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝐵 ⊆ 𝑧) → (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑧)) |
26 | 25 | ssrdv 3951 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝐵 ⊆ 𝑧) → 𝐴 ⊆ 𝑧) |
27 | 26 | ex 414 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 → 𝐴 ⊆ 𝑧)) |
28 | 27 | ss2rabdv 4034 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
29 | 2, 28 | eqsstrid 3993 |
. . 3
⊢ (𝜑 → {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
30 | | intss 4931 |
. . 3
⊢ ({𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} → ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} ⊆ ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤}) |
31 | 29, 30 | syl 17 |
. 2
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ⊆ ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤}) |
32 | | sseq2 3971 |
. . . 4
⊢ (𝑤 = ∩
{𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} → (𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧})) |
33 | | ssorduni 7714 |
. . . . . . . . 9
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
34 | 15, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Ord ∪ 𝐴) |
35 | | ordsuc 7749 |
. . . . . . . 8
⊢ (Ord
∪ 𝐴 ↔ Ord suc ∪
𝐴) |
36 | 34, 35 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → Ord suc ∪ 𝐴) |
37 | 14 | uniexd 7680 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐴
∈ V) |
38 | | sucexg 7741 |
. . . . . . . . 9
⊢ (∪ 𝐴
∈ V → suc ∪ 𝐴 ∈ V) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → suc ∪ 𝐴
∈ V) |
40 | | elong 6326 |
. . . . . . . 8
⊢ (suc
∪ 𝐴 ∈ V → (suc ∪ 𝐴
∈ On ↔ Ord suc ∪ 𝐴)) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (suc ∪ 𝐴
∈ On ↔ Ord suc ∪ 𝐴)) |
42 | 36, 41 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → suc ∪ 𝐴
∈ On) |
43 | | onsucuni 7764 |
. . . . . . 7
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) |
44 | 15, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ suc ∪
𝐴) |
45 | | sseq2 3971 |
. . . . . . 7
⊢ (𝑧 = suc ∪ 𝐴
→ (𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ suc ∪
𝐴)) |
46 | 45 | rspcev 3582 |
. . . . . 6
⊢ ((suc
∪ 𝐴 ∈ On ∧ 𝐴 ⊆ suc ∪
𝐴) → ∃𝑧 ∈ On 𝐴 ⊆ 𝑧) |
47 | 42, 44, 46 | syl2anc 585 |
. . . . 5
⊢ (𝜑 → ∃𝑧 ∈ On 𝐴 ⊆ 𝑧) |
48 | | onintrab2 7733 |
. . . . 5
⊢
(∃𝑧 ∈ On
𝐴 ⊆ 𝑧 ↔ ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈
On) |
49 | 47, 48 | sylib 217 |
. . . 4
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈
On) |
50 | | cofon1.3 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
51 | 32, 49, 50 | elrabd 3648 |
. . 3
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤}) |
52 | | intss1 4925 |
. . 3
⊢ (∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} → ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
53 | 51, 52 | syl 17 |
. 2
⊢ (𝜑 → ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤} ⊆ ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧}) |
54 | 31, 53 | eqssd 3962 |
1
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} = ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤}) |