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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )

Proof

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