wdomtr

Description: Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

		Ref	Expression
	Assertion	wdomtr	⊢ ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) → 𝑋 ≼^* 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		relwdom	⊢ Rel ≼^*
2	1	brrelex2i	⊢ ( 𝑌 ≼^* 𝑍 → 𝑍 ∈ V )
3	2	adantl	⊢ ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) → 𝑍 ∈ V )
4		0wdom	⊢ ( 𝑍 ∈ V → ∅ ≼^* 𝑍 )
5		breq1	⊢ ( 𝑋 = ∅ → ( 𝑋 ≼^* 𝑍 ↔ ∅ ≼^* 𝑍 ) )
6	4 5	syl5ibrcom	⊢ ( 𝑍 ∈ V → ( 𝑋 = ∅ → 𝑋 ≼^* 𝑍 ) )
7	3 6	syl	⊢ ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) → ( 𝑋 = ∅ → 𝑋 ≼^* 𝑍 ) )
8		simpll	⊢ ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) → 𝑋 ≼^* 𝑌 )
9		brwdomn0	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼^* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
10	9	adantl	⊢ ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ≼^* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
11	8 10	mpbid	⊢ ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) → ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 )
12		simpllr	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑌 ≼^* 𝑍 )
13		simplr	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≠ ∅ )
14		dm0rn0	⊢ ( dom 𝑧 = ∅ ↔ ran 𝑧 = ∅ )
15	14	necon3bii	⊢ ( dom 𝑧 ≠ ∅ ↔ ran 𝑧 ≠ ∅ )
16	15	a1i	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ( dom 𝑧 ≠ ∅ ↔ ran 𝑧 ≠ ∅ ) )
17		fof	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝑧 : 𝑌 ⟶ 𝑋 )
18	17	fdmd	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → dom 𝑧 = 𝑌 )
19	18	neeq1d	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ( dom 𝑧 ≠ ∅ ↔ 𝑌 ≠ ∅ ) )
20		forn	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ran 𝑧 = 𝑋 )
21	20	neeq1d	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ( ran 𝑧 ≠ ∅ ↔ 𝑋 ≠ ∅ ) )
22	16 19 21	3bitr3rd	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ( 𝑋 ≠ ∅ ↔ 𝑌 ≠ ∅ ) )
23	22	adantl	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → ( 𝑋 ≠ ∅ ↔ 𝑌 ≠ ∅ ) )
24	13 23	mpbid	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑌 ≠ ∅ )
25		brwdomn0	⊢ ( 𝑌 ≠ ∅ → ( 𝑌 ≼^* 𝑍 ↔ ∃ 𝑦 𝑦 : 𝑍 –onto→ 𝑌 ) )
26	24 25	syl	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → ( 𝑌 ≼^* 𝑍 ↔ ∃ 𝑦 𝑦 : 𝑍 –onto→ 𝑌 ) )
27	12 26	mpbid	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → ∃ 𝑦 𝑦 : 𝑍 –onto→ 𝑌 )
28		vex	⊢ 𝑧 ∈ V
29		vex	⊢ 𝑦 ∈ V
30	28 29	coex	⊢ ( 𝑧 ∘ 𝑦 ) ∈ V
31		foco	⊢ ( ( 𝑧 : 𝑌 –onto→ 𝑋 ∧ 𝑦 : 𝑍 –onto→ 𝑌 ) → ( 𝑧 ∘ 𝑦 ) : 𝑍 –onto→ 𝑋 )
32		fowdom	⊢ ( ( ( 𝑧 ∘ 𝑦 ) ∈ V ∧ ( 𝑧 ∘ 𝑦 ) : 𝑍 –onto→ 𝑋 ) → 𝑋 ≼^* 𝑍 )
33	30 31 32	sylancr	⊢ ( ( 𝑧 : 𝑌 –onto→ 𝑋 ∧ 𝑦 : 𝑍 –onto→ 𝑌 ) → 𝑋 ≼^* 𝑍 )
34	33	adantl	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ ( 𝑧 : 𝑌 –onto→ 𝑋 ∧ 𝑦 : 𝑍 –onto→ 𝑌 ) ) → 𝑋 ≼^* 𝑍 )
35	34	expr	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → ( 𝑦 : 𝑍 –onto→ 𝑌 → 𝑋 ≼^* 𝑍 ) )
36	35	exlimdv	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → ( ∃ 𝑦 𝑦 : 𝑍 –onto→ 𝑌 → 𝑋 ≼^* 𝑍 ) )
37	27 36	mpd	⊢ ( ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼^* 𝑍 )
38	11 37	exlimddv	⊢ ( ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) ∧ 𝑋 ≠ ∅ ) → 𝑋 ≼^* 𝑍 )
39	38	ex	⊢ ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) → ( 𝑋 ≠ ∅ → 𝑋 ≼^* 𝑍 ) )
40	7 39	pm2.61dne	⊢ ( ( 𝑋 ≼^* 𝑌 ∧ 𝑌 ≼^* 𝑍 ) → 𝑋 ≼^* 𝑍 )

Metamath Proof Explorer

Theorem wdomtr

Proof