dihmeetlem1N - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihmeetlem1N		Structured version Unicode version

Theorem dihmeetlem1N 34567

Description: Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dihglblem5a.b
dihglblem5a.m	$./\$
dihglblem5a.h
dihglblem5a.i
dihglblem5a.l
dihglblem5a.j	$.\/$
dihglblem5a.a
dihglblem5a.p
dihglblem5a.t
dihglblem5a.r
dihglblem5a.e
dihglblem5a.g
dihglblem5a.o

**Assertion**
Ref	Expression
dihmeetlem1N	$/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Distinct variable groups: $./\$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

) $.\/$ (

) $./\$ (

)

(

)

(

)

(

)

Proof of Theorem dihmeetlem1N Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1l 1029	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
2		hllat 32638	. . . . . 6
3	1, 2	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp2l 1031	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp3l 1033	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
6		dihglblem5a.b	. . . . . 6
7		dihglblem5a.l	. . . . . 6
8		dihglblem5a.m	. . . . . 6 $./\$
9	6, 7, 8	latmle1 16266	. . . . 5 $/\$ $/\$ $./\$
10	3, 4, 5, 9	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
11		simp1 1005	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	6, 8	latmcl 16242	. . . . . 6 $/\$ $/\$ $./\$
13	3, 4, 5, 12	syl3anc 1264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
14		dihglblem5a.h	. . . . . 6
15		dihglblem5a.i	. . . . . 6
16	6, 7, 14, 15	dihord 34541	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17	11, 13, 4, 16	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
18	10, 17	mpbird 235	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
19	6, 7, 8	latmle2 16267	. . . . 5 $/\$ $/\$ $./\$
20	3, 4, 5, 19	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
21	6, 7, 14, 15	dihord 34541	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
22	11, 13, 5, 21	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
23	20, 22	mpbird 235	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
24	18, 23	ssind 3683	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
25	14, 15	dihvalrel 34556	. . . . 5 $/\$
26		relin1 4962	. . . . 5
27	25, 26	syl 17	. . . 4 $/\$
28	27	3ad2ant1 1026	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
29		elin 3646	. . . 4 $/\$
30		dihglblem5a.j	. . . . . . 7 $.\/$
31		dihglblem5a.a	. . . . . . 7
32	6, 7, 30, 8, 31, 14	lhpmcvr2 33298	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	32	3adant3 1025	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34		simpl1 1008	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35		simpl2 1009	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
36		simprl 762	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simprrl 772	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
38	36, 37	jca 534	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
39		simprrr 773	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40		dihglblem5a.p	. . . . . . . . 9
41		dihglblem5a.t	. . . . . . . . 9
42		dihglblem5a.r	. . . . . . . . 9
43		dihglblem5a.e	. . . . . . . . 9
44		dihglblem5a.g	. . . . . . . . 9
45		vex 3081	. . . . . . . . 9
46		vex 3081	. . . . . . . . 9
47	6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46	dihopelvalc 34526	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48	34, 35, 38, 39, 47	syl112anc 1268	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49		simpr 462	. . . . . . 7 $/\$ $/\$
50	48, 49	syl6bi 231	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		simpl3 1010	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
52		dihglblem5a.o	. . . . . . . . 9
53	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34515	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
54	34, 51, 53	syl2anc 665	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
55	54	biimpd 210	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simprll 770	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3ad2ant3 1028	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
58		simp3rr 1079	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
59	58	fveq1d 5874	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
60		simp11 1035	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	7, 31, 14, 40	lhpocnel2 33293	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2l 1031	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
64		simp2rl 1074	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
65	7, 31, 14, 41, 44	ltrniotacl 33855	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 62, 63, 64, 65	syl112anc 1268	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
67	52, 6	tendo02 34063	. . . . . . . . . . . . . . . . . 18
68	66, 67	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
69	59, 68	eqtrd 2461	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
70	69	cnveqd 5021	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
71		cnvresid 5662	. . . . . . . . . . . . . . 15
72	70, 71	syl6eq 2477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
73	72	coeq2d 5008	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
74	6, 14, 41	ltrn1o 33398	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	60, 57, 74	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
76		f1of 5822	. . . . . . . . . . . . . 14
77		fcoi1 5765	. . . . . . . . . . . . . 14
78	75, 76, 77	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
79	73, 78	eqtrd 2461	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
80	79	fveq2d 5876	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
81		simp3l 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqbrtrrd 4439	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
83		simprlr 771	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	83	3ad2ant3 1028	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
85		simp11l 1116	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
86	85, 2	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
87	6, 14, 41, 42	trlcl 33439	. . . . . . . . . . . 12 $/\$ $/\$
88	60, 57, 87	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
89		simp12l 1118	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
90		simp13l 1120	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
91	6, 7, 8	latlem12 16268	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $./\$
92	86, 88, 89, 90, 91	syl13anc 1266	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
93	82, 84, 92	mpbi2and 929	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
94	57, 93	jca 534	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
95	86, 89, 90, 12	syl3anc 1264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
96		simp11r 1117	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
97	6, 14	lhpbase 33272	. . . . . . . . . . 11
98	96, 97	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
99	86, 89, 90, 19	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
100		simp13r 1121	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
101	6, 7, 86, 95, 90, 98, 99, 100	lattrd 16248	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
102	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34515	. . . . . . . . 9 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$ $/\$ $./\$ $/\$
103	60, 95, 101, 102	syl12anc 1262	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$
104	94, 58, 103	mpbir2and 930	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
105	104	3expia 1207	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $./\$
106	50, 55, 105	syl2and 485	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
107	33, 106	rexlimddv 2919	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
108	29, 107	syl5bi 220	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
109	28, 108	relssdv 4938	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
110	24, 109	eqssd 3478	1 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

wrex 2774

cin 3432

wss 3433

cop 3999 class class class wbr 4417

cmpt 4475

cid 4755

ccnv 4844

cres 4847

ccom 4849

wrel 4850

wf 5588

wf1o 5591

cfv 5592

crio 6257 (class class class)co 6296

cbs 15073

cple 15149

coc 15150

cjn 16133

cmee 16134

clat 16235

catm 32538

chlt 32625

clh 33258

cltrn 33375

ctrl 33433

ctendo 34028

cdih 34505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-riotaBAD 32234

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-iin 4296 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-tpos 6972 df-undef 7019 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-oadd 7185 df-er 7362 df-map 7473 df-en 7569 df-dom 7570 df-sdom 7571 df-fin 7572 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-nn 10599 df-2 10657 df-3 10658 df-4 10659 df-5 10660 df-6 10661 df-n0 10859 df-z 10927 df-uz 11149 df-fz 11772 df-struct 15075 df-ndx 15076 df-slot 15077 df-base 15078 df-sets 15079 df-ress 15080 df-plusg 15155 df-mulr 15156 df-sca 15158 df-vsca 15159 df-0g 15292 df-preset 16117 df-poset 16135 df-plt 16148 df-lub 16164 df-glb 16165 df-join 16166 df-meet 16167 df-p0 16229 df-p1 16230 df-lat 16236 df-clat 16298 df-mgm 16432 df-sgrp 16471 df-mnd 16481 df-submnd 16527 df-grp 16617 df-minusg 16618 df-sbg 16619 df-subg 16758 df-cntz 16915 df-lsm 17216 df-cmn 17360 df-abl 17361 df-mgp 17652 df-ur 17664 df-ring 17710 df-oppr 17779 df-dvdsr 17797 df-unit 17798 df-invr 17828 df-dvr 17839 df-drng 17905 df-lmod 18021 df-lss 18084 df-lsp 18123 df-lvec 18254 df-oposet 32451 df-ol 32453 df-oml 32454 df-covers 32541 df-ats 32542 df-atl 32573 df-cvlat 32597 df-hlat 32626 df-llines 32772 df-lplanes 32773 df-lvols 32774 df-lines 32775 df-psubsp 32777 df-pmap 32778 df-padd 33070 df-lhyp 33262 df-laut 33263 df-ldil 33378 df-ltrn 33379 df-trl 33434 df-tendo 34031 df-edring 34033 df-disoa 34306 df-dvech 34356 df-dib 34416 df-dic 34450 df-dih 34506

This theorem is referenced by: dihmeetbN 34580

W3C validator