Step | Hyp | Ref
| Expression |
1 | | sseq2 4003 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ 𝑧)) |
2 | 1 | cbvrabv 3436 |
. . . 4
⊢ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} = {𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧} |
3 | | sseq1 4002 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) |
4 | 3 | rexbidv 3172 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦)) |
5 | | cofon1.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
6 | 5 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
7 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝑎 ∈ 𝐴) |
8 | 4, 6, 7 | rspcdva 3607 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦) |
9 | | sseq2 4003 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → (𝑎 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑏)) |
10 | 9 | cbvrexvw 3229 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐵 𝑎 ⊆ 𝑦 ↔ ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
11 | 8, 10 | sylib 217 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
12 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝐵 ⊆ 𝑧) |
13 | 12 | sselda 3977 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑧) |
14 | | cofon1.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ 𝒫 On) |
15 | 14 | elpwid 4606 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ On) |
16 | 15 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝐴 ⊆ On) |
17 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ 𝐴) |
18 | 16, 17 | sseldd 3978 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ On) |
19 | | simpllr 773 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → 𝑧 ∈ On) |
20 | | ontr2 6404 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ On ∧ 𝑧 ∈ On) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧) → 𝑎 ∈ 𝑧)) |
21 | 18, 19, 20 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑧) → 𝑎 ∈ 𝑧)) |
22 | 13, 21 | mpan2d 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) ∧ 𝑏 ∈ 𝐵) → (𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧)) |
23 | 22 | rexlimdva 3149 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑧)) |
24 | 11, 23 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ (𝐵 ⊆ 𝑧 ∧ 𝑎 ∈ 𝐴)) → 𝑎 ∈ 𝑧) |
25 | 24 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝐵 ⊆ 𝑧) → (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑧)) |
26 | 25 | ssrdv 3983 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝐵 ⊆ 𝑧) → 𝐴 ⊆ 𝑧) |
27 | 26 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 → 𝐴 ⊆ 𝑧)) |
28 | 27 | ss2rabdv 4068 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ On ∣ 𝐵 ⊆ 𝑧} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
29 | 2, 28 | eqsstrid 4025 |
. . 3
⊢ (𝜑 → {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
30 | | intss 4966 |
. . 3
⊢ ({𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} → ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} ⊆ ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤}) |
31 | 29, 30 | syl 17 |
. 2
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ⊆ ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤}) |
32 | | sseq2 4003 |
. . . 4
⊢ (𝑤 = ∩
{𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} → (𝐵 ⊆ 𝑤 ↔ 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧})) |
33 | | ssorduni 7762 |
. . . . . . . . 9
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
34 | 15, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Ord ∪ 𝐴) |
35 | | ordsuc 7797 |
. . . . . . . 8
⊢ (Ord
∪ 𝐴 ↔ Ord suc ∪
𝐴) |
36 | 34, 35 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → Ord suc ∪ 𝐴) |
37 | 14 | uniexd 7728 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝐴
∈ V) |
38 | | sucexg 7789 |
. . . . . . . . 9
⊢ (∪ 𝐴
∈ V → suc ∪ 𝐴 ∈ V) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → suc ∪ 𝐴
∈ V) |
40 | | elong 6365 |
. . . . . . . 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 7812 |
. . . . . . 7
⊢ (𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴) |
44 | 15, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ suc ∪
𝐴) |
45 | | sseq2 4003 |
. . . . . . 7
⊢ (𝑧 = suc ∪ 𝐴
→ (𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ suc ∪
𝐴)) |
46 | 45 | rspcev 3606 |
. . . . . 6
⊢ ((suc
∪ 𝐴 ∈ On ∧ 𝐴 ⊆ suc ∪
𝐴) → ∃𝑧 ∈ On 𝐴 ⊆ 𝑧) |
47 | 42, 44, 46 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → ∃𝑧 ∈ On 𝐴 ⊆ 𝑧) |
48 | | onintrab2 7781 |
. . . . 5
⊢
(∃𝑧 ∈ On
𝐴 ⊆ 𝑧 ↔ ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈
On) |
49 | 47, 48 | sylib 217 |
. . . 4
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈
On) |
50 | | cofon1.3 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
51 | 32, 49, 50 | elrabd 3680 |
. . 3
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤}) |
52 | | intss1 4960 |
. . 3
⊢ (∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} ∈ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} → ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤} ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) |
53 | 51, 52 | syl 17 |
. 2
⊢ (𝜑 → ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤} ⊆ ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧}) |
54 | 31, 53 | eqssd 3994 |
1
⊢ (𝜑 → ∩ {𝑧
∈ On ∣ 𝐴 ⊆
𝑧} = ∩ {𝑤
∈ On ∣ 𝐵 ⊆
𝑤}) |