Metamath Proof Explorer

Theorem pjoml2

Description: Variation of orthomodular law. Definition in Kalmbach p. 22. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoml2 ⊢A∈Cℋ∧B∈Cℋ∧A⊆B→A∨ℋ⊥⁡A∩B=B

Proof

Step Hyp Ref Expression
1 sseq1 ⊢A=ifA∈CℋA0ℋ→A⊆B↔ifA∈CℋA0ℋ⊆B
2 id ⊢A=ifA∈CℋA0ℋ→A=ifA∈CℋA0ℋ
3 fveq2 ⊢A=ifA∈CℋA0ℋ→⊥⁡A=⊥⁡ifA∈CℋA0ℋ
4 3 ineq1d ⊢A=ifA∈CℋA0ℋ→⊥⁡A∩B=⊥⁡ifA∈CℋA0ℋ∩B
5 2 4 oveq12d ⊢A=ifA∈CℋA0ℋ→A∨ℋ⊥⁡A∩B=ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B
6 5 eqeq1d ⊢A=ifA∈CℋA0ℋ→A∨ℋ⊥⁡A∩B=B↔ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B=B
7 1 6 imbi12d ⊢A=ifA∈CℋA0ℋ→A⊆B→A∨ℋ⊥⁡A∩B=B↔ifA∈CℋA0ℋ⊆B→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B=B
8 sseq2 ⊢B=ifB∈CℋB0ℋ→ifA∈CℋA0ℋ⊆B↔ifA∈CℋA0ℋ⊆ifB∈CℋB0ℋ
9 ineq2 ⊢B=ifB∈CℋB0ℋ→⊥⁡ifA∈CℋA0ℋ∩B=⊥⁡ifA∈CℋA0ℋ∩ifB∈CℋB0ℋ
10 9 oveq2d ⊢B=ifB∈CℋB0ℋ→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B=ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩ifB∈CℋB0ℋ
11 id ⊢B=ifB∈CℋB0ℋ→B=ifB∈CℋB0ℋ
12 10 11 eqeq12d ⊢B=ifB∈CℋB0ℋ→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B=B↔ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩ifB∈CℋB0ℋ=ifB∈CℋB0ℋ
13 8 12 imbi12d ⊢B=ifB∈CℋB0ℋ→ifA∈CℋA0ℋ⊆B→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩B=B↔ifA∈CℋA0ℋ⊆ifB∈CℋB0ℋ→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩ifB∈CℋB0ℋ=ifB∈CℋB0ℋ
14 h0elch ⊢0ℋ∈Cℋ
15 14 elimel ⊢ifA∈CℋA0ℋ∈Cℋ
16 14 elimel ⊢ifB∈CℋB0ℋ∈Cℋ
17 15 16 pjoml2i ⊢ifA∈CℋA0ℋ⊆ifB∈CℋB0ℋ→ifA∈CℋA0ℋ∨ℋ⊥⁡ifA∈CℋA0ℋ∩ifB∈CℋB0ℋ=ifB∈CℋB0ℋ
18 7 13 17 dedth2h ⊢A∈Cℋ∧B∈Cℋ→A⊆B→A∨ℋ⊥⁡A∩B=B
19 18 3impia ⊢A∈Cℋ∧B∈Cℋ∧A⊆B→A∨ℋ⊥⁡A∩B=B