Theorem domtr

Description: Transitivity of dominance relation. Theorem 17 of Suppes p. 94. (Contributed by NM, 4-Jun-1998) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Assertion	domtr	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2		vex	⊢ 𝑦 ∈ V
3	2	brdom	⊢ ( 𝑥 ≼ 𝑦 ↔ ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 )
4		vex	⊢ 𝑧 ∈ V
5	4	brdom	⊢ ( 𝑦 ≼ 𝑧 ↔ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 )
6		exdistrv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) ↔ ( ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 ) )
7		f1co	⊢ ( ( 𝑓 : 𝑦 –1-1→ 𝑧 ∧ 𝑔 : 𝑥 –1-1→ 𝑦 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 )
8	7	ancoms	⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 )
9		vex	⊢ 𝑓 ∈ V
10		vex	⊢ 𝑔 ∈ V
11	9 10	coex	⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
12		f1eq1	⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ : 𝑥 –1-1→ 𝑧 ↔ ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 ) )
13	11 12	spcev	⊢ ( ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 → ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
14	8 13	syl	⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
15	4	brdom	⊢ ( 𝑥 ≼ 𝑧 ↔ ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
16	14 15	sylibr	⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
17	16	exlimivv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
18	6 17	sylbir	⊢ ( ( ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
19	3 5 18	syl2anb	⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧 ) → 𝑥 ≼ 𝑧 )
20	1 19	vtoclr	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )