Metamath Proof Explorer

Theorem mdsymlem5

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢A∈Cℋ
mdsymlem1.2 ⊢B∈Cℋ
mdsymlem1.3 ⊢C=A∨ℋp
Assertion mdsymlem5 ⊢q∈HAtoms∧r∈HAtoms→¬q=p→p⊆q∨ℋr∧q⊆A∧r⊆B→c∈Cℋ∧A⊆c∧p∈HAtoms→p⊆c→p⊆c∩B∨ℋA

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ⊢A∈Cℋ
2 mdsymlem1.2 ⊢B∈Cℋ
3 mdsymlem1.3 ⊢C=A∨ℋp
4 df-ne ⊢q≠p↔¬q=p
5 atnemeq0 ⊢q∈HAtoms∧p∈HAtoms→q≠p↔q∩p=0ℋ
6 4 5 bitr3id ⊢q∈HAtoms∧p∈HAtoms→¬q=p↔q∩p=0ℋ
7 6 anbi2d ⊢q∈HAtoms∧p∈HAtoms→p⊆q∨ℋr∧¬q=p↔p⊆q∨ℋr∧q∩p=0ℋ
8 7 3adant3 ⊢q∈HAtoms∧p∈HAtoms∧r∈HAtoms→p⊆q∨ℋr∧¬q=p↔p⊆q∨ℋr∧q∩p=0ℋ
9 atelch ⊢q∈HAtoms→q∈Cℋ
10 atexch ⊢q∈Cℋ∧p∈HAtoms∧r∈HAtoms→p⊆q∨ℋr∧q∩p=0ℋ→r⊆q∨ℋp
11 9 10 syl3an1 ⊢q∈HAtoms∧p∈HAtoms∧r∈HAtoms→p⊆q∨ℋr∧q∩p=0ℋ→r⊆q∨ℋp
12 8 11 sylbid ⊢q∈HAtoms∧p∈HAtoms∧r∈HAtoms→p⊆q∨ℋr∧¬q=p→r⊆q∨ℋp
13 12 expd ⊢q∈HAtoms∧p∈HAtoms∧r∈HAtoms→p⊆q∨ℋr→¬q=p→r⊆q∨ℋp
14 13 3com23 ⊢q∈HAtoms∧r∈HAtoms∧p∈HAtoms→p⊆q∨ℋr→¬q=p→r⊆q∨ℋp
15 14 3expa ⊢q∈HAtoms∧r∈HAtoms∧p∈HAtoms→p⊆q∨ℋr→¬q=p→r⊆q∨ℋp
16 15 adantrl ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→p⊆q∨ℋr→¬q=p→r⊆q∨ℋp
17 16 adantrd ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→p⊆q∨ℋr∧q⊆A∧r⊆B→¬q=p→r⊆q∨ℋp
18 17 imp32 ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→r⊆q∨ℋp
19 18 adantrl ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→r⊆q∨ℋp
20 19 adantrr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆q∨ℋp
21 simplrl ⊢p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→q⊆A
22 atelch ⊢p∈HAtoms→p∈Cℋ
23 22 anim1i ⊢p∈HAtoms∧c∈Cℋ→p∈Cℋ∧c∈Cℋ
24 23 ancoms ⊢c∈Cℋ∧p∈HAtoms→p∈Cℋ∧c∈Cℋ
25 chub2 ⊢A∈Cℋ∧c∈Cℋ→A⊆c∨ℋA
26 1 25 mpan ⊢c∈Cℋ→A⊆c∨ℋA
27 sstr ⊢q⊆A∧A⊆c∨ℋA→q⊆c∨ℋA
28 26 27 sylan2 ⊢q⊆A∧c∈Cℋ→q⊆c∨ℋA
29 chub1 ⊢c∈Cℋ∧A∈Cℋ→c⊆c∨ℋA
30 1 29 mpan2 ⊢c∈Cℋ→c⊆c∨ℋA
31 sstr ⊢p⊆c∧c⊆c∨ℋA→p⊆c∨ℋA
32 30 31 sylan2 ⊢p⊆c∧c∈Cℋ→p⊆c∨ℋA
33 28 32 anim12i ⊢q⊆A∧c∈Cℋ∧p⊆c∧c∈Cℋ→q⊆c∨ℋA∧p⊆c∨ℋA
34 33 anandirs ⊢q⊆A∧p⊆c∧c∈Cℋ→q⊆c∨ℋA∧p⊆c∨ℋA
35 34 ancoms ⊢c∈Cℋ∧q⊆A∧p⊆c→q⊆c∨ℋA∧p⊆c∨ℋA
36 35 adantll ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧q⊆A∧p⊆c→q⊆c∨ℋA∧p⊆c∨ℋA
37 chjcl ⊢c∈Cℋ∧A∈Cℋ→c∨ℋA∈Cℋ
38 1 37 mpan2 ⊢c∈Cℋ→c∨ℋA∈Cℋ
39 chlub ⊢q∈Cℋ∧p∈Cℋ∧c∨ℋA∈Cℋ→q⊆c∨ℋA∧p⊆c∨ℋA↔q∨ℋp⊆c∨ℋA
40 38 39 syl3an3 ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ→q⊆c∨ℋA∧p⊆c∨ℋA↔q∨ℋp⊆c∨ℋA
41 40 3expa ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ→q⊆c∨ℋA∧p⊆c∨ℋA↔q∨ℋp⊆c∨ℋA
42 41 adantr ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧q⊆A∧p⊆c→q⊆c∨ℋA∧p⊆c∨ℋA↔q∨ℋp⊆c∨ℋA
43 36 42 mpbid ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧q⊆A∧p⊆c→q∨ℋp⊆c∨ℋA
44 43 adantrl ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧A⊆c∧q⊆A∧p⊆c→q∨ℋp⊆c∨ℋA
45 chlejb2 ⊢A∈Cℋ∧c∈Cℋ→A⊆c↔c∨ℋA=c
46 1 45 mpan ⊢c∈Cℋ→A⊆c↔c∨ℋA=c
47 46 biimpa ⊢c∈Cℋ∧A⊆c→c∨ℋA=c
48 47 ad2ant2lr ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧A⊆c∧q⊆A∧p⊆c→c∨ℋA=c
49 44 48 sseqtrd ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ∧A⊆c∧q⊆A∧p⊆c→q∨ℋp⊆c
50 49 exp45 ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ→A⊆c→q⊆A→p⊆c→q∨ℋp⊆c
51 50 anasss ⊢q∈Cℋ∧p∈Cℋ∧c∈Cℋ→A⊆c→q⊆A→p⊆c→q∨ℋp⊆c
52 9 24 51 syl2an ⊢q∈HAtoms∧c∈Cℋ∧p∈HAtoms→A⊆c→q⊆A→p⊆c→q∨ℋp⊆c
53 52 adantlr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→A⊆c→q⊆A→p⊆c→q∨ℋp⊆c
54 21 53 syl7 ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→A⊆c→p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→p⊆c→q∨ℋp⊆c
55 54 imp44 ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→q∨ℋp⊆c
56 20 55 sstrd ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆c
57 simplrr ⊢p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→r⊆B
58 57 ad2antlr ⊢A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆B
59 58 adantl ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆B
60 56 59 ssind ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆c∩B
61 atelch ⊢r∈HAtoms→r∈Cℋ
62 9 61 anim12i ⊢q∈HAtoms∧r∈HAtoms→q∈Cℋ∧r∈Cℋ
63 chincl ⊢c∈Cℋ∧B∈Cℋ→c∩B∈Cℋ
64 2 63 mpan2 ⊢c∈Cℋ→c∩B∈Cℋ
65 chlej1 ⊢r∈Cℋ∧c∩B∈Cℋ∧q∈Cℋ∧r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
66 65 ex ⊢r∈Cℋ∧c∩B∈Cℋ∧q∈Cℋ→r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
67 64 66 syl3an2 ⊢r∈Cℋ∧c∈Cℋ∧q∈Cℋ→r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
68 67 3comr ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ→r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
69 68 3expa ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ→r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
70 69 adantr ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→r⊆c∩B→r∨ℋq⊆c∩B∨ℋq
71 chlej2 ⊢q∈Cℋ∧A∈Cℋ∧c∩B∈Cℋ∧q⊆A→c∩B∨ℋq⊆c∩B∨ℋA
72 1 71 mp3anl2 ⊢q∈Cℋ∧c∩B∈Cℋ∧q⊆A→c∩B∨ℋq⊆c∩B∨ℋA
73 64 72 sylanl2 ⊢q∈Cℋ∧c∈Cℋ∧q⊆A→c∩B∨ℋq⊆c∩B∨ℋA
74 73 adantllr ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→c∩B∨ℋq⊆c∩B∨ℋA
75 sstr2 ⊢r∨ℋq⊆c∩B∨ℋq→c∩B∨ℋq⊆c∩B∨ℋA→r∨ℋq⊆c∩B∨ℋA
76 74 75 syl5com ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→r∨ℋq⊆c∩B∨ℋq→r∨ℋq⊆c∩B∨ℋA
77 chjcom ⊢q∈Cℋ∧r∈Cℋ→q∨ℋr=r∨ℋq
78 77 ad2antrr ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→q∨ℋr=r∨ℋq
79 78 sseq1d ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→q∨ℋr⊆c∩B∨ℋA↔r∨ℋq⊆c∩B∨ℋA
80 76 79 sylibrd ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→r∨ℋq⊆c∩B∨ℋq→q∨ℋr⊆c∩B∨ℋA
81 70 80 syld ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧q⊆A→r⊆c∩B→q∨ℋr⊆c∩B∨ℋA
82 81 adantrl ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧p⊆q∨ℋr∧q⊆A→r⊆c∩B→q∨ℋr⊆c∩B∨ℋA
83 sstr2 ⊢p⊆q∨ℋr→q∨ℋr⊆c∩B∨ℋA→p⊆c∩B∨ℋA
84 83 ad2antrl ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧p⊆q∨ℋr∧q⊆A→q∨ℋr⊆c∩B∨ℋA→p⊆c∩B∨ℋA
85 82 84 syld ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ∧p⊆q∨ℋr∧q⊆A→r⊆c∩B→p⊆c∩B∨ℋA
86 85 exp32 ⊢q∈Cℋ∧r∈Cℋ∧c∈Cℋ→p⊆q∨ℋr→q⊆A→r⊆c∩B→p⊆c∩B∨ℋA
87 62 86 sylan ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ→p⊆q∨ℋr→q⊆A→r⊆c∩B→p⊆c∩B∨ℋA
88 87 adantrr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→p⊆q∨ℋr→q⊆A→r⊆c∩B→p⊆c∩B∨ℋA
89 88 imp31 ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧p⊆q∨ℋr∧q⊆A→r⊆c∩B→p⊆c∩B∨ℋA
90 89 adantrr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧p⊆q∨ℋr∧q⊆A∧r⊆B→r⊆c∩B→p⊆c∩B∨ℋA
91 90 anasss ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧p⊆q∨ℋr∧q⊆A∧r⊆B→r⊆c∩B→p⊆c∩B∨ℋA
92 91 adantrr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→r⊆c∩B→p⊆c∩B∨ℋA
93 92 adantrl ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→r⊆c∩B→p⊆c∩B∨ℋA
94 93 adantrr ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→r⊆c∩B→p⊆c∩B∨ℋA
95 60 94 mpd ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms∧A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p∧p⊆c→p⊆c∩B∨ℋA
96 95 exp32 ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→A⊆c∧p⊆q∨ℋr∧q⊆A∧r⊆B∧¬q=p→p⊆c→p⊆c∩B∨ℋA
97 96 exp4d ⊢q∈HAtoms∧r∈HAtoms∧c∈Cℋ∧p∈HAtoms→A⊆c→p⊆q∨ℋr∧q⊆A∧r⊆B→¬q=p→p⊆c→p⊆c∩B∨ℋA
98 97 exp32 ⊢q∈HAtoms∧r∈HAtoms→c∈Cℋ→p∈HAtoms→A⊆c→p⊆q∨ℋr∧q⊆A∧r⊆B→¬q=p→p⊆c→p⊆c∩B∨ℋA
99 98 com34 ⊢q∈HAtoms∧r∈HAtoms→c∈Cℋ→A⊆c→p∈HAtoms→p⊆q∨ℋr∧q⊆A∧r⊆B→¬q=p→p⊆c→p⊆c∩B∨ℋA
100 99 imp4c ⊢q∈HAtoms∧r∈HAtoms→c∈Cℋ∧A⊆c∧p∈HAtoms→p⊆q∨ℋr∧q⊆A∧r⊆B→¬q=p→p⊆c→p⊆c∩B∨ℋA
101 100 com24 ⊢q∈HAtoms∧r∈HAtoms→¬q=p→p⊆q∨ℋr∧q⊆A∧r⊆B→c∈Cℋ∧A⊆c∧p∈HAtoms→p⊆c→p⊆c∩B∨ℋA