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 → ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) )