Metamath Proof Explorer

Theorem largei

Description: A Hilbert lattice admits a largei set of states. Remark in Mayet p. 370. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypothesis large.1 ⊢ A ∈ C ℋ
Assertion largei ⊢ ¬ A = 0 ℋ ↔ ∃ f ∈ States f ⁡ A = 1

Proof

Step Hyp Ref Expression
1 large.1 ⊢ A ∈ C ℋ
2 ralnex ⊢ ∀ f ∈ States ¬ f ⁡ A = 1 ↔ ¬ ∃ f ∈ States f ⁡ A = 1
3 ax-1ne0 ⊢ 1 ≠ 0
4 3 neii ⊢ ¬ 1 = 0
5 st0 ⊢ f ∈ States → f ⁡ 0 ℋ = 0
6 5 eqeq1d ⊢ f ∈ States → f ⁡ 0 ℋ = 1 ↔ 0 = 1
7 eqcom ⊢ 0 = 1 ↔ 1 = 0
8 6 7 bitrdi ⊢ f ∈ States → f ⁡ 0 ℋ = 1 ↔ 1 = 0
9 4 8 mtbiri ⊢ f ∈ States → ¬ f ⁡ 0 ℋ = 1
10 mtt ⊢ ¬ f ⁡ 0 ℋ = 1 → ¬ f ⁡ A = 1 ↔ f ⁡ A = 1 → f ⁡ 0 ℋ = 1
11 9 10 syl ⊢ f ∈ States → ¬ f ⁡ A = 1 ↔ f ⁡ A = 1 → f ⁡ 0 ℋ = 1
12 11 ralbiia ⊢ ∀ f ∈ States ¬ f ⁡ A = 1 ↔ ∀ f ∈ States f ⁡ A = 1 → f ⁡ 0 ℋ = 1
13 h0elch ⊢ 0 ℋ ∈ C ℋ
14 1 13 strb ⊢ ∀ f ∈ States f ⁡ A = 1 → f ⁡ 0 ℋ = 1 ↔ A ⊆ 0 ℋ
15 1 chle0i ⊢ A ⊆ 0 ℋ ↔ A = 0 ℋ
16 12 14 15 3bitri ⊢ ∀ f ∈ States ¬ f ⁡ A = 1 ↔ A = 0 ℋ
17 2 16 bitr3i ⊢ ¬ ∃ f ∈ States f ⁡ A = 1 ↔ A = 0 ℋ
18 17 con1bii ⊢ ¬ A = 0 ℋ ↔ ∃ f ∈ States f ⁡ A = 1