Metamath Proof Explorer

Theorem mayetes3i

Description: Mayet's equation E^*_3, derived from E_3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of Mayet3 p. 1240. (Contributed by NM, 10-May-2009) (New usage is discouraged.)

Ref Expression
Hypotheses mayetes3.a ⊢ 𝐴 ∈ Cℋ
mayetes3.b ⊢ 𝐵 ∈ Cℋ
mayetes3.c ⊢ 𝐶 ∈ Cℋ
mayetes3.d ⊢ 𝐷 ∈ Cℋ
mayetes3.f ⊢ 𝐹 ∈ Cℋ
mayetes3.g ⊢ 𝐺 ∈ Cℋ
mayetes3.r ⊢ 𝑅 ∈ Cℋ
mayetes3.ac ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐶 )
mayetes3.af ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐹 )
mayetes3.cf ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐹 )
mayetes3.ab ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
mayetes3.cd ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
mayetes3.fg ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
mayetes3.rx ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝑋 )
mayetes3.x ⊢ 𝑋 = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
mayetes3.y ⊢ 𝑌 = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) )
mayetes3.z ⊢ 𝑍 = ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
Assertion mayetes3i ( ( 𝑋 ∨ℋ 𝑅 ) ∩ 𝑌 ) ⊆ ( 𝑍 ∨ℋ 𝑅 )

Proof

Step Hyp Ref Expression
1 mayetes3.a ⊢ 𝐴 ∈ Cℋ
2 mayetes3.b ⊢ 𝐵 ∈ Cℋ
3 mayetes3.c ⊢ 𝐶 ∈ Cℋ
4 mayetes3.d ⊢ 𝐷 ∈ Cℋ
5 mayetes3.f ⊢ 𝐹 ∈ Cℋ
6 mayetes3.g ⊢ 𝐺 ∈ Cℋ
7 mayetes3.r ⊢ 𝑅 ∈ Cℋ
8 mayetes3.ac ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐶 )
9 mayetes3.af ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐹 )
10 mayetes3.cf ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐹 )
11 mayetes3.ab ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
12 mayetes3.cd ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
13 mayetes3.fg ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
14 mayetes3.rx ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝑋 )
15 mayetes3.x ⊢ 𝑋 = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
16 mayetes3.y ⊢ 𝑌 = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) )
17 mayetes3.z ⊢ 𝑍 = ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
18 1 3 chjcli ⊢ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ
19 18 5 chjcli ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∈ Cℋ
20 19 7 chjcomi ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) = ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) )
21 20 eqimssi ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) )
22 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
23 22 7 chub1i ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ 𝑅 )
24 1 2 7 chjassi ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ 𝑅 ) = ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) )
25 23 24 sseqtri ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) )
26 2 7 chjcli ⊢ ( 𝐵 ∨ℋ 𝑅 ) ∈ Cℋ
27 1 26 chjcli ⊢ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∈ Cℋ
28 27 7 chub2i ⊢ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ⊆ ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) )
29 25 28 sstri ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) )
30 3 4 chjcli ⊢ ( 𝐶 ∨ℋ 𝐷 ) ∈ Cℋ
31 30 7 chub1i ⊢ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝑅 )
32 3 4 7 chjassi ⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ∨ℋ 𝑅 ) = ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
33 31 32 sseqtri ⊢ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
34 4 7 chjcli ⊢ ( 𝐷 ∨ℋ 𝑅 ) ∈ Cℋ
35 3 34 chjcli ⊢ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ∈ Cℋ
36 35 7 chub2i ⊢ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) )
37 33 36 sstri ⊢ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) )
38 ss2in ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) )
39 29 37 38 mp2an ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) )
40 5 6 chjcli ⊢ ( 𝐹 ∨ℋ 𝐺 ) ∈ Cℋ
41 40 7 chub1i ⊢ ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
42 5 6 7 chjassi ⊢ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) = ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
43 41 42 sseqtri ⊢ ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
44 6 7 chjcli ⊢ ( 𝐺 ∨ℋ 𝑅 ) ∈ Cℋ
45 5 44 chjcli ⊢ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ∈ Cℋ
46 45 7 chub2i ⊢ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ⊆ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) )
47 43 46 sstri ⊢ ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) )
48 ss2in ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∧ ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ⊆ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
49 39 47 48 mp2an ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ⊆ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) )
50 ss2in ⊢ ( ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ⊆ ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∧ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ⊆ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) → ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ∩ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ) ⊆ ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) )
51 21 49 50 mp2an ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ∩ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ) ⊆ ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
52 27 35 chincli ⊢ ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∈ Cℋ
53 52 45 chincli ⊢ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ∈ Cℋ
54 15 19 eqeltri ⊢ 𝑋 ∈ Cℋ
55 54 choccli ⊢ ( ⊥ ‘ 𝑋 ) ∈ Cℋ
56 7 55 14 lecmii ⊢ 𝑅 𝐶ℋ ( ⊥ ‘ 𝑋 )
57 7 54 cmcm2i ⊢ ( 𝑅 𝐶ℋ 𝑋 ↔ 𝑅 𝐶ℋ ( ⊥ ‘ 𝑋 ) )
58 56 57 mpbir ⊢ 𝑅 𝐶ℋ 𝑋
59 58 15 breqtri ⊢ 𝑅 𝐶ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
60 7 2 chub2i ⊢ 𝑅 ⊆ ( 𝐵 ∨ℋ 𝑅 )
61 26 1 chub2i ⊢ ( 𝐵 ∨ℋ 𝑅 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) )
62 60 61 sstri ⊢ 𝑅 ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) )
63 7 27 62 lecmii ⊢ 𝑅 𝐶ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) )
64 7 4 chub2i ⊢ 𝑅 ⊆ ( 𝐷 ∨ℋ 𝑅 )
65 34 3 chub2i ⊢ ( 𝐷 ∨ℋ 𝑅 ) ⊆ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
66 64 65 sstri ⊢ 𝑅 ⊆ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
67 7 35 66 lecmii ⊢ 𝑅 𝐶ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
68 7 27 35 63 67 cm2mi ⊢ 𝑅 𝐶ℋ ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) )
69 7 6 chub2i ⊢ 𝑅 ⊆ ( 𝐺 ∨ℋ 𝑅 )
70 44 5 chub2i ⊢ ( 𝐺 ∨ℋ 𝑅 ) ⊆ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
71 69 70 sstri ⊢ 𝑅 ⊆ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
72 7 45 71 lecmii ⊢ 𝑅 𝐶ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
73 7 52 45 68 72 cm2mi ⊢ 𝑅 𝐶ℋ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) )
74 7 19 53 59 73 fh3i ⊢ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) = ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
75 7 52 45 68 72 fh3i ⊢ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) = ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) )
76 7 27 35 63 67 fh3i ⊢ ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) = ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) )
77 76 ineq1i ⊢ ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) = ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) )
78 75 77 eqtri ⊢ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) = ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) )
79 78 ineq2i ⊢ ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) = ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
80 74 79 eqtr2i ⊢ ( ( 𝑅 ∨ℋ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ) ∩ ( ( ( 𝑅 ∨ℋ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ) ∩ ( 𝑅 ∨ℋ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) = ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
81 51 80 sseqtri ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ∩ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ) ⊆ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) )
82 2 4 chjcli ⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Cℋ
83 82 6 chjcli ⊢ ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∈ Cℋ
84 7 83 chub2i ⊢ 𝑅 ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
85 1 3 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 )
86 18 5 chub1i ⊢ ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
87 86 15 sseqtrri ⊢ ( 𝐴 ∨ℋ 𝐶 ) ⊆ 𝑋
88 85 87 sstri ⊢ 𝐴 ⊆ 𝑋
89 1 54 chsscon3i ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐴 ) )
90 88 89 mpbi ⊢ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐴 )
91 14 90 sstri ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐴 )
92 7 1 chsscon2i ⊢ ( 𝑅 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊆ ( ⊥ ‘ 𝑅 ) )
93 91 92 mpbi ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝑅 )
94 11 93 ssini ⊢ 𝐴 ⊆ ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝑅 ) )
95 2 7 chdmj1i ⊢ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝑅 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝑅 ) )
96 94 95 sseqtrri ⊢ 𝐴 ⊆ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝑅 ) )
97 3 1 chub2i ⊢ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 )
98 97 87 sstri ⊢ 𝐶 ⊆ 𝑋
99 3 54 chsscon3i ⊢ ( 𝐶 ⊆ 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐶 ) )
100 98 99 mpbi ⊢ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐶 )
101 14 100 sstri ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐶 )
102 7 3 chsscon2i ⊢ ( 𝑅 ⊆ ( ⊥ ‘ 𝐶 ) ↔ 𝐶 ⊆ ( ⊥ ‘ 𝑅 ) )
103 101 102 mpbi ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝑅 )
104 12 103 ssini ⊢ 𝐶 ⊆ ( ( ⊥ ‘ 𝐷 ) ∩ ( ⊥ ‘ 𝑅 ) )
105 4 7 chdmj1i ⊢ ( ⊥ ‘ ( 𝐷 ∨ℋ 𝑅 ) ) = ( ( ⊥ ‘ 𝐷 ) ∩ ( ⊥ ‘ 𝑅 ) )
106 104 105 sseqtrri ⊢ 𝐶 ⊆ ( ⊥ ‘ ( 𝐷 ∨ℋ 𝑅 ) )
107 5 18 chub2i ⊢ 𝐹 ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
108 107 15 sseqtrri ⊢ 𝐹 ⊆ 𝑋
109 5 54 chsscon3i ⊢ ( 𝐹 ⊆ 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐹 ) )
110 108 109 mpbi ⊢ ( ⊥ ‘ 𝑋 ) ⊆ ( ⊥ ‘ 𝐹 )
111 14 110 sstri ⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐹 )
112 7 5 chsscon2i ⊢ ( 𝑅 ⊆ ( ⊥ ‘ 𝐹 ) ↔ 𝐹 ⊆ ( ⊥ ‘ 𝑅 ) )
113 111 112 mpbi ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝑅 )
114 13 113 ssini ⊢ 𝐹 ⊆ ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝑅 ) )
115 6 7 chdmj1i ⊢ ( ⊥ ‘ ( 𝐺 ∨ℋ 𝑅 ) ) = ( ( ⊥ ‘ 𝐺 ) ∩ ( ⊥ ‘ 𝑅 ) )
116 114 115 sseqtrri ⊢ 𝐹 ⊆ ( ⊥ ‘ ( 𝐺 ∨ℋ 𝑅 ) )
117 eqid ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
118 eqid ⊢ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) = ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) )
119 82 6 7 chjjdiri ⊢ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) = ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝑅 ) ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
120 2 4 7 chjjdiri ⊢ ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝑅 ) = ( ( 𝐵 ∨ℋ 𝑅 ) ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) )
121 120 oveq1i ⊢ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝑅 ) ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) = ( ( ( 𝐵 ∨ℋ 𝑅 ) ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
122 119 121 eqtri ⊢ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) = ( ( ( 𝐵 ∨ℋ 𝑅 ) ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) )
123 1 26 3 34 5 44 8 9 10 96 106 116 117 118 122 mayete3i ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
124 19 53 chincli ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ∈ Cℋ
125 83 7 chjcli ⊢ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) ∈ Cℋ
126 7 124 125 chlubii ⊢ ( ( 𝑅 ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) ∧ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) ) → ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 ) )
127 84 123 126 mp2an ⊢ ( 𝑅 ∨ℋ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∩ ( ( ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝑅 ) ) ∩ ( 𝐶 ∨ℋ ( 𝐷 ∨ℋ 𝑅 ) ) ) ∩ ( 𝐹 ∨ℋ ( 𝐺 ∨ℋ 𝑅 ) ) ) ) ) ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
128 81 127 sstri ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ∩ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) ) ⊆ ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
129 15 oveq1i ⊢ ( 𝑋 ∨ℋ 𝑅 ) = ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 )
130 129 16 ineq12i ⊢ ( ( 𝑋 ∨ℋ 𝑅 ) ∩ 𝑌 ) = ( ( ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∨ℋ 𝑅 ) ∩ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) ) )
131 17 oveq1i ⊢ ( 𝑍 ∨ℋ 𝑅 ) = ( ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 ) ∨ℋ 𝑅 )
132 128 130 131 3sstr4i ⊢ ( ( 𝑋 ∨ℋ 𝑅 ) ∩ 𝑌 ) ⊆ ( 𝑍 ∨ℋ 𝑅 )