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 𝐶 )