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 ⊢ A ∈ V ∧ B ∈ W ∧ N ∈ ℕ 0 ∧ ¬ B ∈ A → N < A ↔ N + 1 < A ∪ B

Proof

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