ssdomg

Description: A set dominates its subsets. Theorem 16 of Suppes p. 94. (Contributed by NM, 19-Jun-1998) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	ssdomg	$⊢ B \in V \to (A \subseteq B \to A ≼ B)$

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
2		simpr	$⊢ (A \subseteq B \land B \in V) \to B \in V$
3		f1oi	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A$
4		dff1o3	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A \leftrightarrow (({I ↾}_{A}) : A \underset{onto}{⟶} A \land Fun {({I ↾}_{A})}^{-1})$
5	3 4	mpbi	$⊢ (({I ↾}_{A}) : A \underset{onto}{⟶} A \land Fun {({I ↾}_{A})}^{-1})$
6	5	simpli	$⊢ ({I ↾}_{A}) : A \underset{onto}{⟶} A$
7		fof	$⊢ ({I ↾}_{A}) : A \underset{onto}{⟶} A \to ({I ↾}_{A}) : A ⟶ A$
8	6 7	ax-mp	$⊢ ({I ↾}_{A}) : A ⟶ A$
9		fss	$⊢ (({I ↾}_{A}) : A ⟶ A \land A \subseteq B) \to ({I ↾}_{A}) : A ⟶ B$
10	8 9	mpan	$⊢ A \subseteq B \to ({I ↾}_{A}) : A ⟶ B$
11		funi	$⊢ Fun I$
12		cnvi	$⊢ I^{-1} = I$
13	12	funeqi	$⊢ Fun I^{-1} \leftrightarrow Fun I$
14	11 13	mpbir	$⊢ Fun I^{-1}$
15		funres11	$⊢ Fun I^{-1} \to Fun {({I ↾}_{A})}^{-1}$
16	14 15	ax-mp	$⊢ Fun {({I ↾}_{A})}^{-1}$
17		df-f1	$⊢ ({I ↾}_{A}) : A \underset{1-1}{⟶} B \leftrightarrow (({I ↾}_{A}) : A ⟶ B \land Fun {({I ↾}_{A})}^{-1})$
18	10 16 17	sylanblrc	$⊢ A \subseteq B \to ({I ↾}_{A}) : A \underset{1-1}{⟶} B$
19	18	adantr	$⊢ (A \subseteq B \land B \in V) \to ({I ↾}_{A}) : A \underset{1-1}{⟶} B$
20		f1dom2g	$⊢ (A \in V \land B \in V \land ({I ↾}_{A}) : A \underset{1-1}{⟶} B) \to A ≼ B$
21	1 2 19 20	syl3anc	$⊢ (A \subseteq B \land B \in V) \to A ≼ B$
22	21	expcom	$⊢ B \in V \to (A \subseteq B \to A ≼ B)$

Metamath Proof Explorer