Metamath Proof Explorer

Theorem hashpss

Description: The size of a proper subset is less than the size of its finite superset. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Assertion hashpss ⊢ A ∈ Fin ∧ B ⊂ A → B < A

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ Fin ∧ B ⊂ A → A ∈ Fin
2 simpr ⊢ A ∈ Fin ∧ B ⊂ A → B ⊂ A
3 2 pssssd ⊢ A ∈ Fin ∧ B ⊂ A → B ⊆ A
4 1 3 ssexd ⊢ A ∈ Fin ∧ B ⊂ A → B ∈ V
5 hashxrcl ⊢ B ∈ V → B ∈ ℝ *
6 4 5 syl ⊢ A ∈ Fin ∧ B ⊂ A → B ∈ ℝ *
7 hashxrcl ⊢ A ∈ Fin → A ∈ ℝ *
8 7 adantr ⊢ A ∈ Fin ∧ B ⊂ A → A ∈ ℝ *
9 hashss ⊢ A ∈ Fin ∧ B ⊆ A → B ≤ A
10 3 9 syldan ⊢ A ∈ Fin ∧ B ⊂ A → B ≤ A
11 1 adantr ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → A ∈ Fin
12 3 adantr ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B ⊆ A
13 11 12 ssfid ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B ∈ Fin
14 simpr ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → A = B
15 hashen ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ A ≈ B
16 15 biimpa ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A = B → A ≈ B
17 11 13 14 16 syl21anc ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → A ≈ B
18 17 ensymd ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B ≈ A
19 fisseneq ⊢ A ∈ Fin ∧ B ⊆ A ∧ B ≈ A → B = A
20 11 12 18 19 syl3anc ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B = A
21 2 adantr ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B ⊂ A
22 21 pssned ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → B ≠ A
23 22 neneqd ⊢ A ∈ Fin ∧ B ⊂ A ∧ A = B → ¬ B = A
24 20 23 pm2.65da ⊢ A ∈ Fin ∧ B ⊂ A → ¬ A = B
25 24 neqned ⊢ A ∈ Fin ∧ B ⊂ A → A ≠ B
26 xrltlen ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B < A ↔ B ≤ A ∧ A ≠ B
27 26 biimpar ⊢ B ∈ ℝ * ∧ A ∈ ℝ * ∧ B ≤ A ∧ A ≠ B → B < A
28 6 8 10 25 27 syl22anc ⊢ A ∈ Fin ∧ B ⊂ A → B < A