Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐵 =
∪ 𝐵 |
2 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐶 =
∪ 𝐶 |
3 | 1, 2 | refbas 22407 |
. . 3
⊢ (𝐵Ref𝐶 → ∪ 𝐶 = ∪
𝐵) |
4 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐴 =
∪ 𝐴 |
5 | 4, 1 | refbas 22407 |
. . 3
⊢ (𝐴Ref𝐵 → ∪ 𝐵 = ∪
𝐴) |
6 | 3, 5 | sylan9eqr 2800 |
. 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → ∪ 𝐶 = ∪
𝐴) |
7 | | refssex 22408 |
. . . . . 6
⊢ ((𝐴Ref𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) |
8 | 7 | ex 416 |
. . . . 5
⊢ (𝐴Ref𝐵 → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
9 | 8 | adantr 484 |
. . . 4
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
10 | | refssex 22408 |
. . . . . . 7
⊢ ((𝐵Ref𝐶 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧) |
11 | 10 | ad2ant2lr 748 |
. . . . . 6
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → ∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧) |
12 | | sstr2 3908 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝑦 → (𝑦 ⊆ 𝑧 → 𝑥 ⊆ 𝑧)) |
13 | 12 | reximdv 3192 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝑦 → (∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) |
14 | 13 | ad2antll 729 |
. . . . . 6
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → (∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) |
15 | 11, 14 | mpd 15 |
. . . . 5
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧) |
16 | 15 | rexlimdvaa 3204 |
. . . 4
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) |
17 | 9, 16 | syld 47 |
. . 3
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝑥 ∈ 𝐴 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) |
18 | 17 | ralrimiv 3104 |
. 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧) |
19 | | refrel 22405 |
. . . . 5
⊢ Rel
Ref |
20 | 19 | brrelex1i 5605 |
. . . 4
⊢ (𝐴Ref𝐵 → 𝐴 ∈ V) |
21 | 20 | adantr 484 |
. . 3
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴 ∈ V) |
22 | 4, 2 | isref 22406 |
. . 3
⊢ (𝐴 ∈ V → (𝐴Ref𝐶 ↔ (∪ 𝐶 = ∪
𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧))) |
23 | 21, 22 | syl 17 |
. 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝐴Ref𝐶 ↔ (∪ 𝐶 = ∪
𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧))) |
24 | 6, 18, 23 | mpbir2and 713 |
1
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴Ref𝐶) |