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 ∈ V → A ⊆ B → A ≼ B

Proof

Step Hyp Ref Expression
1 ssexg ⊢ A ⊆ B ∧ B ∈ V → A ∈ V
2 simpr ⊢ A ⊆ B ∧ B ∈ V → B ∈ V
3 f1oi ⊢ I ↾ A : A ⟶ 1-1 onto A
4 dff1o3 ⊢ I ↾ A : A ⟶ 1-1 onto A ↔ I ↾ A : A ⟶ onto A ∧ Fun ⁡ I ↾ A -1
5 3 4 mpbi ⊢ I ↾ A : A ⟶ onto A ∧ Fun ⁡ I ↾ A -1
6 5 simpli ⊢ I ↾ A : A ⟶ onto A
7 fof ⊢ I ↾ A : A ⟶ onto A → I ↾ A : A ⟶ A
8 6 7 ax-mp ⊢ I ↾ A : A ⟶ A
9 fss ⊢ I ↾ A : A ⟶ A ∧ A ⊆ B → I ↾ A : A ⟶ B
10 8 9 mpan ⊢ A ⊆ B → I ↾ A : A ⟶ B
11 funi ⊢ Fun ⁡ I
12 cnvi ⊢ I -1 = I
13 12 funeqi ⊢ Fun ⁡ I -1 ↔ Fun ⁡ I
14 11 13 mpbir ⊢ Fun ⁡ I -1
15 funres11 ⊢ Fun ⁡ I -1 → Fun ⁡ I ↾ A -1
16 14 15 ax-mp ⊢ Fun ⁡ I ↾ A -1
17 df-f1 ⊢ I ↾ A : A ⟶ 1-1 B ↔ I ↾ A : A ⟶ B ∧ Fun ⁡ I ↾ A -1
18 10 16 17 sylanblrc ⊢ A ⊆ B → I ↾ A : A ⟶ 1-1 B
19 18 adantr ⊢ A ⊆ B ∧ B ∈ V → I ↾ A : A ⟶ 1-1 B
20 f1dom2g ⊢ A ∈ V ∧ B ∈ V ∧ I ↾ A : A ⟶ 1-1 B → A ≼ B
21 1 2 19 20 syl3anc ⊢ A ⊆ B ∧ B ∈ V → A ≼ B
22 21 expcom ⊢ B ∈ V → A ⊆ B → A ≼ B