Metamath Proof Explorer

Theorem tgldimor

Description: Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019)

Ref Expression
Hypotheses tgldimor.p ⊢ 𝑃 = ( 𝐸 ‘ 𝐹 )
tgldimor.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
Assertion tgldimor ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 tgldimor.p ⊢ 𝑃 = ( 𝐸 ‘ 𝐹 )
2 tgldimor.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
3 1 fvexi ⊢ 𝑃 ∈ V
4 hashv01gt1 ⊢ ( 𝑃 ∈ V → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) )
5 3 4 ax-mp ⊢ ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) )
6 3orass ⊢ ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) ↔ ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) ) )
7 5 6 mpbi ⊢ ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) )
8 1p1e2 ⊢ ( 1 + 1 ) = 2
9 1z ⊢ 1 ∈ ℤ
10 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
11 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℤ ) → ( 1 < ( ♯ ‘ 𝑃 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
12 9 10 11 sylancr ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝑃 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
13 12 biimpac ⊢ ( ( 1 < ( ♯ ‘ 𝑃 ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) )
14 8 13 eqbrtrrid ⊢ ( ( 1 < ( ♯ ‘ 𝑃 ) ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ0 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
15 2re ⊢ 2 ∈ ℝ
16 15 rexri ⊢ 2 ∈ ℝ*
17 pnfge ⊢ ( 2 ∈ ℝ* → 2 ≤ +∞ )
18 16 17 ax-mp ⊢ 2 ≤ +∞
19 breq2 ⊢ ( ( ♯ ‘ 𝑃 ) = +∞ → ( 2 ≤ ( ♯ ‘ 𝑃 ) ↔ 2 ≤ +∞ ) )
20 18 19 mpbiri ⊢ ( ( ♯ ‘ 𝑃 ) = +∞ → 2 ≤ ( ♯ ‘ 𝑃 ) )
21 20 adantl ⊢ ( ( 1 < ( ♯ ‘ 𝑃 ) ∧ ( ♯ ‘ 𝑃 ) = +∞ ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
22 hashnn0pnf ⊢ ( 𝑃 ∈ V → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑃 ) = +∞ ) )
23 3 22 mp1i ⊢ ( 1 < ( ♯ ‘ 𝑃 ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑃 ) = +∞ ) )
24 14 21 23 mpjaodan ⊢ ( 1 < ( ♯ ‘ 𝑃 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
25 24 orim2i ⊢ ( ( ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
26 25 orim2i ⊢ ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 1 < ( ♯ ‘ 𝑃 ) ) ) → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) )
27 7 26 mp1i ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) )
28 ne0i ⊢ ( 𝐴 ∈ 𝑃 → 𝑃 ≠ ∅ )
29 hasheq0 ⊢ ( 𝑃 ∈ V → ( ( ♯ ‘ 𝑃 ) = 0 ↔ 𝑃 = ∅ ) )
30 3 29 ax-mp ⊢ ( ( ♯ ‘ 𝑃 ) = 0 ↔ 𝑃 = ∅ )
31 30 biimpi ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → 𝑃 = ∅ )
32 31 necon3ai ⊢ ( 𝑃 ≠ ∅ → ¬ ( ♯ ‘ 𝑃 ) = 0 )
33 2 28 32 3syl ⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝑃 ) = 0 )
34 biorf ⊢ ( ¬ ( ♯ ‘ 𝑃 ) = 0 → ( ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ↔ ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) ) )
35 33 34 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ↔ ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) ) ) )
36 27 35 mpbird ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )