This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjoml6i

Description: An equivalent of the orthomodular law. Theorem 29.13(e) of MaedaMaeda p. 132. (Contributed by NM, 30-May-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion pjoml6i ( 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4 3 2 chincli ⊢ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ
5 1 2 pjoml2i ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = 𝐵 )
6 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
7 1 6 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) )
8 1 2 chdmm2i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) )
9 7 8 sseqtrri ⊢ 𝐴 ⊆ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) )
10 5 9 jctil ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ⊆ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∧ ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = 𝐵 ) )
11 fveq2 ⊢ ( 𝑥 = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
12 11 sseq2d ⊢ ( 𝑥 = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ) )
13 oveq2 ⊢ ( 𝑥 = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) )
14 13 eqeq1d ⊢ ( 𝑥 = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ↔ ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = 𝐵 ) )
15 12 14 anbi12d ⊢ ( 𝑥 = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) → ( ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ↔ ( 𝐴 ⊆ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∧ ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = 𝐵 ) ) )
16 15 rspcev ⊢ ( ( ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ⊆ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) ∧ ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) = 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )
17 4 10 16 sylancr ⊢ ( 𝐴 ⊆ 𝐵 → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )