Metamath Proof Explorer

Theorem reftr

Description: Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Assertion reftr ⊢ A Ref B ∧ B Ref C → A Ref C

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ B = ⋃ B
2 eqid ⊢ ⋃ C = ⋃ C
3 1 2 refbas ⊢ B Ref C → ⋃ C = ⋃ B
4 eqid ⊢ ⋃ A = ⋃ A
5 4 1 refbas ⊢ A Ref B → ⋃ B = ⋃ A
6 3 5 sylan9eqr ⊢ A Ref B ∧ B Ref C → ⋃ C = ⋃ A
7 refssex ⊢ A Ref B ∧ x ∈ A → ∃ y ∈ B x ⊆ y
8 7 ex ⊢ A Ref B → x ∈ A → ∃ y ∈ B x ⊆ y
9 8 adantr ⊢ A Ref B ∧ B Ref C → x ∈ A → ∃ y ∈ B x ⊆ y
10 refssex ⊢ B Ref C ∧ y ∈ B → ∃ z ∈ C y ⊆ z
11 10 ad2ant2lr ⊢ A Ref B ∧ B Ref C ∧ y ∈ B ∧ x ⊆ y → ∃ z ∈ C y ⊆ z
12 sstr2 ⊢ x ⊆ y → y ⊆ z → x ⊆ z
13 12 reximdv ⊢ x ⊆ y → ∃ z ∈ C y ⊆ z → ∃ z ∈ C x ⊆ z
14 13 ad2antll ⊢ A Ref B ∧ B Ref C ∧ y ∈ B ∧ x ⊆ y → ∃ z ∈ C y ⊆ z → ∃ z ∈ C x ⊆ z
15 11 14 mpd ⊢ A Ref B ∧ B Ref C ∧ y ∈ B ∧ x ⊆ y → ∃ z ∈ C x ⊆ z
16 15 rexlimdvaa ⊢ A Ref B ∧ B Ref C → ∃ y ∈ B x ⊆ y → ∃ z ∈ C x ⊆ z
17 9 16 syld ⊢ A Ref B ∧ B Ref C → x ∈ A → ∃ z ∈ C x ⊆ z
18 17 ralrimiv ⊢ A Ref B ∧ B Ref C → ∀ x ∈ A ∃ z ∈ C x ⊆ z
19 refrel ⊢ Rel ⁡ Ref
20 19 brrelex1i ⊢ A Ref B → A ∈ V
21 20 adantr ⊢ A Ref B ∧ B Ref C → A ∈ V
22 4 2 isref ⊢ A ∈ V → A Ref C ↔ ⋃ C = ⋃ A ∧ ∀ x ∈ A ∃ z ∈ C x ⊆ z
23 21 22 syl ⊢ A Ref B ∧ B Ref C → A Ref C ↔ ⋃ C = ⋃ A ∧ ∀ x ∈ A ∃ z ∈ C x ⊆ z
24 6 18 23 mpbir2and ⊢ A Ref B ∧ B Ref C → A Ref C