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