Theorem chirredlem4

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chirred.1	⊢ 𝐴 ∈ Cℋ
	chirred.2	⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
Assertion	chirredlem4	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) )

Proof

Step	Hyp	Ref	Expression
1		chirred.1	⊢ 𝐴 ∈ Cℋ
2		chirred.2	⊢ ( 𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥 )
3		atelch	⊢ ( 𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
4		breq2	⊢ ( 𝑥 = 𝑟 → ( 𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑟 ) )
5	4 2	vtoclga	⊢ ( 𝑟 ∈ Cℋ → 𝐴 𝐶ℋ 𝑟 )
6	3 5	syl	⊢ ( 𝑟 ∈ HAtoms → 𝐴 𝐶ℋ 𝑟 )
7	1	atordi	⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝑟 ) → ( 𝑟 ⊆ 𝐴 ∨ 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) ) )
8	6 7	mpdan	⊢ ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ 𝐴 ∨ 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) ) )
9	8	ad2antrl	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ 𝐴 ∨ 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) ) )
10	1 2	chirredlem3	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ 𝐴 → 𝑟 = 𝑝 ) )
11	1	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
12	11	sseq2i	⊢ ( 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ↔ 𝑝 ⊆ 𝐴 )
13	12	biimpri	⊢ ( 𝑝 ⊆ 𝐴 → 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
14		atelch	⊢ ( 𝑞 ∈ HAtoms → 𝑞 ∈ Cℋ )
15		atelch	⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
16		chjcom	⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) → ( 𝑞 ∨ℋ 𝑝 ) = ( 𝑝 ∨ℋ 𝑞 ) )
17	14 15 16	syl2an	⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( 𝑞 ∨ℋ 𝑝 ) = ( 𝑝 ∨ℋ 𝑞 ) )
18	17	sseq2d	⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ↔ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) )
19	18	anbi2d	⊢ ( ( 𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ↔ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
20	19	ad2ant2r	⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ↔ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) )
21	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
22		cmcm3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 𝐶ℋ 𝑥 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝑥 ) )
23	1 22	mpan	⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 𝐶ℋ 𝑥 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝑥 ) )
24	2 23	mpbid	⊢ ( 𝑥 ∈ Cℋ → ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝑥 )
25	21 24	chirredlem3	⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) )
26	25	ex	⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑞 ∨ℋ 𝑝 ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) ) )
27	20 26	sylbird	⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) ) )
28	13 27	sylanr2	⊢ ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ) → ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) ) )
29	28	imp	⊢ ( ( ( ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) )
30	29	ancom1s	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) → 𝑟 = 𝑞 ) )
31	10 30	orim12d	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( 𝑟 ⊆ 𝐴 ∨ 𝑟 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) ) )
32	9 31	mpd	⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ HAtoms ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑟 = 𝑝 ∨ 𝑟 = 𝑞 ) )