This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐵 ∈ 𝑉 → ( 𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵 ) )

Proof

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