Metamath Proof Explorer


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 ∧ 𝑟 ⊆ ( 𝑝 𝑞 ) ) ) → ( 𝑟 = 𝑝𝑟 = 𝑞 ) )