This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → 𝐴 Ref 𝐶 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐵 = ∪ 𝐵
2 eqid ⊢ ∪ 𝐶 = ∪ 𝐶
3 1 2 refbas ⊢ ( 𝐵 Ref 𝐶 → ∪ 𝐶 = ∪ 𝐵 )
4 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
5 4 1 refbas ⊢ ( 𝐴 Ref 𝐵 → ∪ 𝐵 = ∪ 𝐴 )
6 3 5 sylan9eqr ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ∪ 𝐶 = ∪ 𝐴 )
7 refssex ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
8 7 ex ⊢ ( 𝐴 Ref 𝐵 → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
9 8 adantr ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
10 refssex ⊢ ( ( 𝐵 Ref 𝐶 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 )
11 10 ad2ant2lr ⊢ ( ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 )
12 sstr2 ⊢ ( 𝑥 ⊆ 𝑦 → ( 𝑦 ⊆ 𝑧 → 𝑥 ⊆ 𝑧 ) )
13 12 reximdv ⊢ ( 𝑥 ⊆ 𝑦 → ( ∃ 𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) )
14 13 ad2antll ⊢ ( ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦 ) ) → ( ∃ 𝑧 ∈ 𝐶 𝑦 ⊆ 𝑧 → ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) )
15 11 14 mpd ⊢ ( ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 )
16 15 rexlimdvaa ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) )
17 9 16 syld ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) )
18 17 ralrimiv ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 )
19 refrel ⊢ Rel Ref
20 19 brrelex1i ⊢ ( 𝐴 Ref 𝐵 → 𝐴 ∈ V )
21 20 adantr ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → 𝐴 ∈ V )
22 4 2 isref ⊢ ( 𝐴 ∈ V → ( 𝐴 Ref 𝐶 ↔ ( ∪ 𝐶 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) ) )
23 21 22 syl ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → ( 𝐴 Ref 𝐶 ↔ ( ∪ 𝐶 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑥 ⊆ 𝑧 ) ) )
24 6 18 23 mpbir2and ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝐵 Ref 𝐶 ) → 𝐴 Ref 𝐶 )