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ℋ ( 𝐴 ⊆ ( ⊥ ‘ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )