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 ⊢ARefB∧BRefC→ARefC

Proof

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