Metamath Proof Explorer

Theorem hashunsnggt

Description: The size of a set is greater than a nonnegative integer N if and only if the size of the union of that set with a disjoint singleton is greater than N + 1. (Contributed by BTernaryTau, 10-Sep-2023)

Ref Expression
Assertion hashunsnggt ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) < ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2 1 rexrd ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ* )
3 hashxrcl ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
4 1re ⊢ 1 ∈ ℝ
5 xltadd1 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 +𝑒 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
6 4 5 mp3an3 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ* ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 +𝑒 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
7 2 3 6 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 +𝑒 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 +𝑒 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
9 rexadd ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑁 +𝑒 1 ) = ( 𝑁 + 1 ) )
10 4 9 mpan2 ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 +𝑒 1 ) = ( 𝑁 + 1 ) )
11 1 10 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 +𝑒 1 ) = ( 𝑁 + 1 ) )
12 11 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 +𝑒 1 ) = ( 𝑁 + 1 ) )
13 12 breq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 +𝑒 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ↔ ( 𝑁 + 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
14 8 13 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
15 14 3adant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
17 hashunsngx ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ∈ 𝐴 → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )
18 17 3impia ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) )
19 18 eqcomd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) = ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
20 19 3expa ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) = ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
21 20 3adantl3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) = ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
22 21 breq2d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ( 𝑁 + 1 ) < ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ↔ ( 𝑁 + 1 ) < ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) ) )
23 16 22 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0 ) ∧ ¬ 𝐵 ∈ 𝐴 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) < ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) ) )