Theorem dfch2

Description: Alternate definition of the Hilbert lattice. (Contributed by NM, 8-Aug-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	dfch2	⊢ Cℋ = { 𝑥 ∈ 𝒫 ℋ ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		chss	⊢ ( 𝑥 ∈ Cℋ → 𝑥 ⊆ ℋ )
2		ococ	⊢ ( 𝑥 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
3	1 2	jca	⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
4		occl	⊢ ( 𝑥 ⊆ ℋ → ( ⊥ ‘ 𝑥 ) ∈ Cℋ )
5		chss	⊢ ( ( ⊥ ‘ 𝑥 ) ∈ Cℋ → ( ⊥ ‘ 𝑥 ) ⊆ ℋ )
6		occl	⊢ ( ( ⊥ ‘ 𝑥 ) ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) ∈ Cℋ )
7	4 5 6	3syl	⊢ ( 𝑥 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) ∈ Cℋ )
8		eleq1	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) ∈ Cℋ ↔ 𝑥 ∈ Cℋ ) )
9	7 8	imbitrid	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 → ( 𝑥 ⊆ ℋ → 𝑥 ∈ Cℋ ) )
10	9	impcom	⊢ ( ( 𝑥 ⊆ ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) → 𝑥 ∈ Cℋ )
11	3 10	impbii	⊢ ( 𝑥 ∈ Cℋ ↔ ( 𝑥 ⊆ ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
12		velpw	⊢ ( 𝑥 ∈ 𝒫 ℋ ↔ 𝑥 ⊆ ℋ )
13	12	anbi1i	⊢ ( ( 𝑥 ∈ 𝒫 ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝑥 ⊆ ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
14	11 13	bitr4i	⊢ ( 𝑥 ∈ Cℋ ↔ ( 𝑥 ∈ 𝒫 ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
15	14	eqabi	⊢ Cℋ = { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) }
16		df-rab	⊢ { 𝑥 ∈ 𝒫 ℋ ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) }
17	15 16	eqtr4i	⊢ Cℋ = { 𝑥 ∈ 𝒫 ℋ ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 }