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

Metamath Proof Explorer

Theorem wdomfil

Description: Weak dominance agrees with normal for finite left sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdomfil ( 𝑋 ∈ Fin → ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 relwdom ⊢ Rel ≼*
2 1 brrelex2i ⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V )
3 0domg ⊢ ( 𝑌 ∈ V → ∅ ≼ 𝑌 )
4 2 3 syl ⊢ ( 𝑋 ≼* 𝑌 → ∅ ≼ 𝑌 )
5 breq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 ≼ 𝑌 ↔ ∅ ≼ 𝑌 ) )
6 4 5 imbitrrid ⊢ ( 𝑋 = ∅ → ( 𝑋 ≼* 𝑌 → 𝑋 ≼ 𝑌 ) )
7 6 adantl ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑋 = ∅ ) → ( 𝑋 ≼* 𝑌 → 𝑋 ≼ 𝑌 ) )
8 brwdomn0 ⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
9 8 adantl ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 ) )
10 vex ⊢ 𝑥 ∈ V
11 fof ⊢ ( 𝑥 : 𝑌 –onto→ 𝑋 → 𝑥 : 𝑌 ⟶ 𝑋 )
12 dmfex ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 : 𝑌 ⟶ 𝑋 ) → 𝑌 ∈ V )
13 10 11 12 sylancr ⊢ ( 𝑥 : 𝑌 –onto→ 𝑋 → 𝑌 ∈ V )
14 13 adantl ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑥 : 𝑌 –onto→ 𝑋 ) → 𝑌 ∈ V )
15 simpl ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑥 : 𝑌 –onto→ 𝑋 ) → 𝑋 ∈ Fin )
16 simpr ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑥 : 𝑌 –onto→ 𝑋 ) → 𝑥 : 𝑌 –onto→ 𝑋 )
17 fodomfi2 ⊢ ( ( 𝑌 ∈ V ∧ 𝑋 ∈ Fin ∧ 𝑥 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼ 𝑌 )
18 14 15 16 17 syl3anc ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑥 : 𝑌 –onto→ 𝑋 ) → 𝑋 ≼ 𝑌 )
19 18 ex ⊢ ( 𝑋 ∈ Fin → ( 𝑥 : 𝑌 –onto→ 𝑋 → 𝑋 ≼ 𝑌 ) )
20 19 adantr ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑋 ≠ ∅ ) → ( 𝑥 : 𝑌 –onto→ 𝑋 → 𝑋 ≼ 𝑌 ) )
21 20 exlimdv ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑥 𝑥 : 𝑌 –onto→ 𝑋 → 𝑋 ≼ 𝑌 ) )
22 9 21 sylbid ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ≼* 𝑌 → 𝑋 ≼ 𝑌 ) )
23 7 22 pm2.61dane ⊢ ( 𝑋 ∈ Fin → ( 𝑋 ≼* 𝑌 → 𝑋 ≼ 𝑌 ) )
24 domwdom ⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌 )
25 23 24 impbid1 ⊢ ( 𝑋 ∈ Fin → ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) )