Metamath Proof Explorer

Theorem hashss

Description: The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018)

Ref Expression
Assertion hashss ⊢ A ∈ V ∧ B ⊆ A → B ≤ A

Proof

Step Hyp Ref Expression
1 ssdomg ⊢ A ∈ Fin → B ⊆ A → B ≼ A
2 1 com12 ⊢ B ⊆ A → A ∈ Fin → B ≼ A
3 2 adantl ⊢ A ∈ V ∧ B ⊆ A → A ∈ Fin → B ≼ A
4 3 impcom ⊢ A ∈ Fin ∧ A ∈ V ∧ B ⊆ A → B ≼ A
5 ssfi ⊢ A ∈ Fin ∧ B ⊆ A → B ∈ Fin
6 5 adantrl ⊢ A ∈ Fin ∧ A ∈ V ∧ B ⊆ A → B ∈ Fin
7 simpl ⊢ A ∈ Fin ∧ A ∈ V ∧ B ⊆ A → A ∈ Fin
8 hashdom ⊢ B ∈ Fin ∧ A ∈ Fin → B ≤ A ↔ B ≼ A
9 6 7 8 syl2anc ⊢ A ∈ Fin ∧ A ∈ V ∧ B ⊆ A → B ≤ A ↔ B ≼ A
10 4 9 mpbird ⊢ A ∈ Fin ∧ A ∈ V ∧ B ⊆ A → B ≤ A
11 10 ex ⊢ A ∈ Fin → A ∈ V ∧ B ⊆ A → B ≤ A
12 hashinf ⊢ A ∈ V ∧ ¬ A ∈ Fin → A = +∞
13 ssexg ⊢ B ⊆ A ∧ A ∈ V → B ∈ V
14 13 ancoms ⊢ A ∈ V ∧ B ⊆ A → B ∈ V
15 hashxrcl ⊢ B ∈ V → B ∈ ℝ *
16 pnfge ⊢ B ∈ ℝ * → B ≤ +∞
17 14 15 16 3syl ⊢ A ∈ V ∧ B ⊆ A → B ≤ +∞
18 17 ex ⊢ A ∈ V → B ⊆ A → B ≤ +∞
19 18 adantl ⊢ A = +∞ ∧ A ∈ V → B ⊆ A → B ≤ +∞
20 breq2 ⊢ A = +∞ → B ≤ A ↔ B ≤ +∞
21 20 adantr ⊢ A = +∞ ∧ A ∈ V → B ≤ A ↔ B ≤ +∞
22 19 21 sylibrd ⊢ A = +∞ ∧ A ∈ V → B ⊆ A → B ≤ A
23 22 expcom ⊢ A ∈ V → A = +∞ → B ⊆ A → B ≤ A
24 23 adantr ⊢ A ∈ V ∧ ¬ A ∈ Fin → A = +∞ → B ⊆ A → B ≤ A
25 12 24 mpd ⊢ A ∈ V ∧ ¬ A ∈ Fin → B ⊆ A → B ≤ A
26 25 impancom ⊢ A ∈ V ∧ B ⊆ A → ¬ A ∈ Fin → B ≤ A
27 26 com12 ⊢ ¬ A ∈ Fin → A ∈ V ∧ B ⊆ A → B ≤ A
28 11 27 pm2.61i ⊢ A ∈ V ∧ B ⊆ A → B ≤ A