| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢ ∪ 𝐵 =
∪ 𝐵 | 
| 2 |  | eqid 2737 | . . . 4
⊢ ∪ 𝐶 =
∪ 𝐶 | 
| 3 | 1, 2 | refbas 23518 | . . 3
⊢ (𝐵Ref𝐶 → ∪ 𝐶 = ∪
𝐵) | 
| 4 |  | eqid 2737 | . . . 4
⊢ ∪ 𝐴 =
∪ 𝐴 | 
| 5 | 4, 1 | refbas 23518 | . . 3
⊢ (𝐴Ref𝐵 → ∪ 𝐵 = ∪
𝐴) | 
| 6 | 3, 5 | sylan9eqr 2799 | . 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → ∪ 𝐶 = ∪
𝐴) | 
| 7 |  | refssex 23519 | . . . . . 6
⊢ ((𝐴Ref𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) | 
| 8 | 7 | ex 412 | . . . . 5
⊢ (𝐴Ref𝐵 → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | 
| 10 |  | refssex 23519 | . . . . . . 7
⊢ ((𝐵Ref𝐶 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧) | 
| 11 | 10 | ad2ant2lr 748 | . . . . . 6
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → ∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧) | 
| 12 |  | sstr2 3990 | . . . . . . . 8
⊢ (𝑥 ⊆ 𝑦 → (𝑦 ⊆ 𝑧 → 𝑥 ⊆ 𝑧)) | 
| 13 | 12 | reximdv 3170 | . . . . . . 7
⊢ (𝑥 ⊆ 𝑦 → (∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) | 
| 14 | 13 | ad2antll 729 | . . . . . 6
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → (∃𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) | 
| 15 | 11, 14 | mpd 15 | . . . . 5
⊢ (((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦)) → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧) | 
| 16 | 15 | rexlimdvaa 3156 | . . . 4
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) | 
| 17 | 9, 16 | syld 47 | . . 3
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝑥 ∈ 𝐴 → ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧)) | 
| 18 | 17 | ralrimiv 3145 | . 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧) | 
| 19 |  | refrel 23516 | . . . . 5
⊢ Rel
Ref | 
| 20 | 19 | brrelex1i 5741 | . . . 4
⊢ (𝐴Ref𝐵 → 𝐴 ∈ V) | 
| 21 | 20 | adantr 480 | . . 3
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴 ∈ V) | 
| 22 | 4, 2 | isref 23517 | . . 3
⊢ (𝐴 ∈ V → (𝐴Ref𝐶 ↔ (∪ 𝐶 = ∪
𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧))) | 
| 23 | 21, 22 | syl 17 | . 2
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → (𝐴Ref𝐶 ↔ (∪ 𝐶 = ∪
𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧))) | 
| 24 | 6, 18, 23 | mpbir2and 713 | 1
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴Ref𝐶) |