dihmeetlem1N - Mathbox for Norm Megill

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

Theorem dihmeetlem1N 31773

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 981	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
2		hllat 29846	. . . . . 6
3	1, 2	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp2l 983	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp3l 985	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
6		dihglblem5a.b	. . . . . 6
7		dihglblem5a.l	. . . . . 6
8		dihglblem5a.m	. . . . . 6 $./\$
9	6, 7, 8	latmle1 14460	. . . . 5 $/\$ $/\$ $./\$
10	3, 4, 5, 9	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
11		simp1 957	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	6, 8	latmcl 14435	. . . . . 6 $/\$ $/\$ $./\$
13	3, 4, 5, 12	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
14		dihglblem5a.h	. . . . . 6
15		dihglblem5a.i	. . . . . 6
16	6, 7, 14, 15	dihord 31747	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17	11, 13, 4, 16	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
18	10, 17	mpbird 224	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
19	6, 7, 8	latmle2 14461	. . . . 5 $/\$ $/\$ $./\$
20	3, 4, 5, 19	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
21	6, 7, 14, 15	dihord 31747	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
22	11, 13, 5, 21	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
23	20, 22	mpbird 224	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
24	18, 23	ssind 3525	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
25	14, 15	dihvalrel 31762	. . . . 5 $/\$
26		relin1 4951	. . . . 5
27	25, 26	syl 16	. . . 4 $/\$
28	27	3ad2ant1 978	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
29		elin 3490	. . . 4 $/\$
30		dihglblem5a.j	. . . . . . 7 $.\/$
31		dihglblem5a.a	. . . . . . 7
32	6, 7, 30, 8, 31, 14	lhpmcvr2 30506	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	32	3adant3 977	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34		simpl1 960	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35		simpl2 961	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
36		simprl 733	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simprrl 741	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
38	36, 37	jca 519	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
39		simprrr 742	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40		dihglblem5a.p	. . . . . . . . 9
41		dihglblem5a.t	. . . . . . . . 9
42		dihglblem5a.r	. . . . . . . . 9
43		dihglblem5a.e	. . . . . . . . 9
44		dihglblem5a.g	. . . . . . . . 9
45		vex 2919	. . . . . . . . 9
46		vex 2919	. . . . . . . . 9
47	6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46	dihopelvalc 31732	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48	34, 35, 38, 39, 47	syl112anc 1188	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49		simpr 448	. . . . . . 7 $/\$ $/\$
50	48, 49	syl6bi 220	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		simpl3 962	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
52		dihglblem5a.o	. . . . . . . . 9
53	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 31721	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
54	34, 51, 53	syl2anc 643	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
55	54	biimpd 199	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simprll 739	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3ad2ant3 980	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
58		simp3rr 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
59	58	fveq1d 5689	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
60		simp11 987	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	7, 31, 14, 40	lhpocnel2 30501	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	60, 61	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2l 983	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
64		simp2rl 1026	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
65	7, 31, 14, 41, 44	ltrniotacl 31061	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 62, 63, 64, 65	syl112anc 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
67	52, 6	tendo02 31269	. . . . . . . . . . . . . . . . . 18
68	66, 67	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
69	59, 68	eqtrd 2436	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
70	69	cnveqd 5007	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
71		cnvresid 5482	. . . . . . . . . . . . . . 15
72	70, 71	syl6eq 2452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
73	72	coeq2d 4994	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
74	6, 14, 41	ltrn1o 30606	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	60, 57, 74	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
76		f1of 5633	. . . . . . . . . . . . . 14
77		fcoi1 5576	. . . . . . . . . . . . . 14
78	75, 76, 77	3syl 19	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
79	73, 78	eqtrd 2436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
80	79	fveq2d 5691	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
81		simp3l 985	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqbrtrrd 4194	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
83		simprlr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	83	3ad2ant3 980	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
85		simp11l 1068	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
86	85, 2	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
87	6, 14, 41, 42	trlcl 30646	. . . . . . . . . . . 12 $/\$ $/\$
88	60, 57, 87	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
89		simp12l 1070	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
90		simp13l 1072	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
91	6, 7, 8	latlem12 14462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $./\$
92	86, 88, 89, 90, 91	syl13anc 1186	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
93	82, 84, 92	mpbi2and 888	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
94	57, 93	jca 519	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
95	86, 89, 90, 12	syl3anc 1184	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
96		simp11r 1069	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
97	6, 14	lhpbase 30480	. . . . . . . . . . 11
98	96, 97	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
99	86, 89, 90, 19	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
100		simp13r 1073	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
101	6, 7, 86, 95, 90, 98, 99, 100	lattrd 14442	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
102	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 31721	. . . . . . . . 9 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$ $/\$ $./\$ $/\$
103	60, 95, 101, 102	syl12anc 1182	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$
104	94, 58, 103	mpbir2and 889	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
105	104	3expia 1155	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $./\$
106	50, 55, 105	syl2and 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
107	33, 106	rexlimddv 2794	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
108	29, 107	syl5bi 209	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
109	28, 108	relssdv 4927	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
110	24, 109	eqssd 3325	1 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wrex 2667

cin 3279

wss 3280

cop 3777 class class class wbr 4172

cmpt 4226

cid 4453

ccnv 4836

cres 4839

ccom 4841

wrel 4842

wf 5409

wf1o 5412

cfv 5413 (class class class)co 6040

crio 6501

cbs 13424

cple 13491

coc 13492

cjn 14356

cmee 14357

clat 14429

catm 29746

chlt 29833

clh 30466

cltrn 30583

ctrl 30640

ctendo 31234

cdih 31711

This theorem is referenced by: dihmeetbN 31786

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-fal 1326 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-tpos 6438 df-undef 6502 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-sca 13500 df-vsca 13501 df-0g 13682 df-poset 14358 df-plt 14370 df-lub 14386 df-glb 14387 df-join 14388 df-meet 14389 df-p0 14423 df-p1 14424 df-lat 14430 df-clat 14492 df-mnd 14645 df-submnd 14694 df-grp 14767 df-minusg 14768 df-sbg 14769 df-subg 14896 df-cntz 15071 df-lsm 15225 df-cmn 15369 df-abl 15370 df-mgp 15604 df-rng 15618 df-ur 15620 df-oppr 15683 df-dvdsr 15701 df-unit 15702 df-invr 15732 df-dvr 15743 df-drng 15792 df-lmod 15907 df-lss 15964 df-lsp 16003 df-lvec 16130 df-oposet 29659 df-ol 29661 df-oml 29662 df-covers 29749 df-ats 29750 df-atl 29781 df-cvlat 29805 df-hlat 29834 df-llines 29980 df-lplanes 29981 df-lvols 29982 df-lines 29983 df-psubsp 29985 df-pmap 29986 df-padd 30278 df-lhyp 30470 df-laut 30471 df-ldil 30586 df-ltrn 30587 df-trl 30641 df-tendo 31237 df-edring 31239 df-disoa 31512 df-dvech 31562 df-dib 31622 df-dic 31656 df-dih 31712

W3C validator