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 𝐴C
Assertion largei ( ¬ 𝐴 = 0 ↔ ∃ 𝑓 ∈ States ( 𝑓𝐴 ) = 1 )

Proof

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