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	$⊢ X \in Fin \to (X ≼^{*} Y \leftrightarrow X ≼ Y)$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex2i	$⊢ X ≼^{*} Y \to Y \in V$
3		0domg	$⊢ Y \in V \to \emptyset ≼ Y$
4	2 3	syl	$⊢ X ≼^{*} Y \to \emptyset ≼ Y$
5		breq1	$⊢ X = \emptyset \to (X ≼ Y \leftrightarrow \emptyset ≼ Y)$
6	4 5	imbitrrid	$⊢ X = \emptyset \to (X ≼^{*} Y \to X ≼ Y)$
7	6	adantl	$⊢ (X \in Fin \land X = \emptyset) \to (X ≼^{*} Y \to X ≼ Y)$
8		brwdomn0	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists x x : Y \underset{onto}{⟶} X)$
9	8	adantl	$⊢ (X \in Fin \land X \neq \emptyset) \to (X ≼^{*} Y \leftrightarrow \exists x x : Y \underset{onto}{⟶} X)$
10		vex	$⊢ x \in V$
11		fof	$⊢ x : Y \underset{onto}{⟶} X \to x : Y ⟶ X$
12		dmfex	$⊢ (x \in V \land x : Y ⟶ X) \to Y \in V$
13	10 11 12	sylancr	$⊢ x : Y \underset{onto}{⟶} X \to Y \in V$
14	13	adantl	$⊢ (X \in Fin \land x : Y \underset{onto}{⟶} X) \to Y \in V$
15		simpl	$⊢ (X \in Fin \land x : Y \underset{onto}{⟶} X) \to X \in Fin$
16		simpr	$⊢ (X \in Fin \land x : Y \underset{onto}{⟶} X) \to x : Y \underset{onto}{⟶} X$
17		fodomfi2	$⊢ (Y \in V \land X \in Fin \land x : Y \underset{onto}{⟶} X) \to X ≼ Y$
18	14 15 16 17	syl3anc	$⊢ (X \in Fin \land x : Y \underset{onto}{⟶} X) \to X ≼ Y$
19	18	ex	$⊢ X \in Fin \to (x : Y \underset{onto}{⟶} X \to X ≼ Y)$
20	19	adantr	$⊢ (X \in Fin \land X \neq \emptyset) \to (x : Y \underset{onto}{⟶} X \to X ≼ Y)$
21	20	exlimdv	$⊢ (X \in Fin \land X \neq \emptyset) \to (\exists x x : Y \underset{onto}{⟶} X \to X ≼ Y)$
22	9 21	sylbid	$⊢ (X \in Fin \land X \neq \emptyset) \to (X ≼^{*} Y \to X ≼ Y)$
23	7 22	pm2.61dane	$⊢ X \in Fin \to (X ≼^{*} Y \to X ≼ Y)$
24		domwdom	$⊢ X ≼ Y \to X ≼^{*} Y$
25	23 24	impbid1	$⊢ X \in Fin \to (X ≼^{*} Y \leftrightarrow X ≼ Y)$

Metamath Proof Explorer

Theorem wdomfil

Proof