# Metamath Proof Explorer

## Theorem 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 \left({A}\subseteq {B}\to {A}\preccurlyeq {B}\right)$

### Proof

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