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