fodomfi2

Description: Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015)

		Ref	Expression
	Assertion	fodomfi2	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$

Proof

Step	Hyp	Ref	Expression
1		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
2	1	3ad2ant3	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to F Fn A$
3		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
4		eqimss2	$⊢ ran F = B \to B \subseteq ran F$
5	3 4	syl	$⊢ F : A \underset{onto}{⟶} B \to B \subseteq ran F$
6	5	3ad2ant3	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to B \subseteq ran F$
7		simp2	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to B \in Fin$
8		fipreima	$⊢ (F Fn A \land B \subseteq ran F \land B \in Fin) \to \exists x \in (𝒫 A \cap Fin) F [x] = B$
9	2 6 7 8	syl3anc	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to \exists x \in (𝒫 A \cap Fin) F [x] = B$
10		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
11	10	adantl	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
12		finnum	$⊢ x \in Fin \to x \in dom card$
13	11 12	syl	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to x \in dom card$
14		simpl3	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to F : A \underset{onto}{⟶} B$
15		fofun	$⊢ F : A \underset{onto}{⟶} B \to Fun F$
16	14 15	syl	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to Fun F$
17		elinel1	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
18	17	elpwid	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
19	18	adantl	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to x \subseteq A$
20		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
21		fdm	$⊢ F : A ⟶ B \to dom F = A$
22	14 20 21	3syl	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to dom F = A$
23	19 22	sseqtrrd	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to x \subseteq dom F$
24		fores	$⊢ (Fun F \land x \subseteq dom F) \to ({F ↾}_{x}) : x \underset{onto}{⟶} F [x]$
25	16 23 24	syl2anc	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to ({F ↾}_{x}) : x \underset{onto}{⟶} F [x]$
26		fodomnum	$⊢ x \in dom card \to (({F ↾}_{x}) : x \underset{onto}{⟶} F [x] \to F [x] ≼ x)$
27	13 25 26	sylc	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to F [x] ≼ x$
28		simpl1	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to A \in V$
29		ssdomg	$⊢ A \in V \to (x \subseteq A \to x ≼ A)$
30	28 19 29	sylc	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to x ≼ A$
31		domtr	$⊢ (F [x] ≼ x \land x ≼ A) \to F [x] ≼ A$
32	27 30 31	syl2anc	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to F [x] ≼ A$
33		breq1	$⊢ F [x] = B \to (F [x] ≼ A \leftrightarrow B ≼ A)$
34	32 33	syl5ibcom	$⊢ ((A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \land x \in (𝒫 A \cap Fin)) \to (F [x] = B \to B ≼ A)$
35	34	rexlimdva	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to (\exists x \in (𝒫 A \cap Fin) F [x] = B \to B ≼ A)$
36	9 35	mpd	$⊢ (A \in V \land B \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$

Metamath Proof Explorer

Theorem fodomfi2

Proof