wdomima2g

Description: A set is weakly dominant over its image under any function. This version of wdomimag is stated so as to avoid ax-rep . (Contributed by Mario Carneiro, 25-Jun-2015)

		Ref	Expression
	Assertion	wdomima2g	$⊢ (Fun F \land A \in V \land F [A] \in W) \to F [A] ≼^{*} A$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
2		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
3		funforn	$⊢ Fun ({F ↾}_{A}) \leftrightarrow ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
4	2 3	sylib	$⊢ Fun F \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
5	4	3ad2ant1	$⊢ (Fun F \land A \in V \land F [A] \in W) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
6		fof	$⊢ ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A}) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ran ({F ↾}_{A})$
7	5 6	syl	$⊢ (Fun F \land A \in V \land F [A] \in W) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ran ({F ↾}_{A})$
8		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
9		inss1	$⊢ A \cap dom F \subseteq A$
10	8 9	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq A$
11		simp2	$⊢ (Fun F \land A \in V \land F [A] \in W) \to A \in V$
12		ssexg	$⊢ (dom ({F ↾}_{A}) \subseteq A \land A \in V) \to dom ({F ↾}_{A}) \in V$
13	10 11 12	sylancr	$⊢ (Fun F \land A \in V \land F [A] \in W) \to dom ({F ↾}_{A}) \in V$
14		simp3	$⊢ (Fun F \land A \in V \land F [A] \in W) \to F [A] \in W$
15	1 14	eqeltrrid	$⊢ (Fun F \land A \in V \land F [A] \in W) \to ran ({F ↾}_{A}) \in W$
16		fex2	$⊢ (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ran ({F ↾}_{A}) \land dom ({F ↾}_{A}) \in V \land ran ({F ↾}_{A}) \in W) \to {F ↾}_{A} \in V$
17	7 13 15 16	syl3anc	$⊢ (Fun F \land A \in V \land F [A] \in W) \to {F ↾}_{A} \in V$
18		fowdom	$⊢ ({F ↾}_{A} \in V \land ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})) \to ran ({F ↾}_{A}) ≼^{*} dom ({F ↾}_{A})$
19	17 5 18	syl2anc	$⊢ (Fun F \land A \in V \land F [A] \in W) \to ran ({F ↾}_{A}) ≼^{*} dom ({F ↾}_{A})$
20		ssdomg	$⊢ A \in V \to (dom ({F ↾}_{A}) \subseteq A \to dom ({F ↾}_{A}) ≼ A)$
21	10 20	mpi	$⊢ A \in V \to dom ({F ↾}_{A}) ≼ A$
22		domwdom	$⊢ dom ({F ↾}_{A}) ≼ A \to dom ({F ↾}_{A}) ≼^{*} A$
23	21 22	syl	$⊢ A \in V \to dom ({F ↾}_{A}) ≼^{*} A$
24	23	3ad2ant2	$⊢ (Fun F \land A \in V \land F [A] \in W) \to dom ({F ↾}_{A}) ≼^{*} A$
25		wdomtr	$⊢ (ran ({F ↾}_{A}) ≼^{} dom ({F ↾}_{A}) \land dom ({F ↾}_{A}) ≼^{} A) \to ran ({F ↾}_{A}) ≼^{*} A$
26	19 24 25	syl2anc	$⊢ (Fun F \land A \in V \land F [A] \in W) \to ran ({F ↾}_{A}) ≼^{*} A$
27	1 26	eqbrtrid	$⊢ (Fun F \land A \in V \land F [A] \in W) \to F [A] ≼^{*} A$

Metamath Proof Explorer

Theorem wdomima2g

Proof