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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴 ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )

Proof

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