Step | Hyp | Ref
| Expression |
1 | | sseq1 4002 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦)) |
2 | 1 | rexbidv 3172 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦)) |
3 | | coflton.4 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
5 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
6 | 2, 4, 5 | rspcdva 3607 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦) |
7 | 6 | adantrr 714 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → ∃𝑦 ∈ 𝐵 𝑎 ⊆ 𝑦) |
8 | | sseq2 4003 |
. . . . 5
⊢ (𝑦 = 𝑏 → (𝑎 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑏)) |
9 | 8 | cbvrexvw 3229 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝑎 ⊆ 𝑦 ↔ ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
10 | 7, 9 | sylib 217 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) |
11 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
12 | | simplrr 775 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → 𝑐 ∈ 𝐶) |
13 | | coflton.5 |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝑧 ∈ 𝑤) |
14 | 13 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝑧 ∈ 𝑤) |
15 | | elequ1 2105 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (𝑧 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤)) |
16 | | elequ2 2113 |
. . . . . . 7
⊢ (𝑤 = 𝑐 → (𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑐)) |
17 | 15, 16 | rspc2va 3618 |
. . . . . 6
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝑧 ∈ 𝑤) → 𝑏 ∈ 𝑐) |
18 | 11, 12, 14, 17 | syl21anc 835 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑐) |
19 | | coflton.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ On) |
20 | 19 | sselda 3977 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ On) |
21 | 20 | adantrr 714 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → 𝑎 ∈ On) |
22 | | coflton.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ On) |
23 | 22 | sselda 3977 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ On) |
24 | 23 | adantrl 713 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → 𝑐 ∈ On) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → 𝑐 ∈ On) |
26 | | ontr2 6404 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑐 ∈ On) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑐) → 𝑎 ∈ 𝑐)) |
27 | 21, 25, 26 | syl2an2r 682 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → ((𝑎 ⊆ 𝑏 ∧ 𝑏 ∈ 𝑐) → 𝑎 ∈ 𝑐)) |
28 | 18, 27 | mpan2d 691 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ∧ 𝑏 ∈ 𝐵) → (𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑐)) |
29 | 28 | rexlimdva 3149 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → (∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏 → 𝑎 ∈ 𝑐)) |
30 | 10, 29 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) → 𝑎 ∈ 𝑐) |
31 | 30 | ralrimivva 3194 |
1
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 𝑎 ∈ 𝑐) |