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 37118

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 1020	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
2		hllat 35189	. . . . . 6
3	1, 2	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp2l 1022	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp3l 1024	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
6		dihglblem5a.b	. . . . . 6
7		dihglblem5a.l	. . . . . 6
8		dihglblem5a.m	. . . . . 6 $./\$
9	6, 7, 8	latmle1 15832	. . . . 5 $/\$ $/\$ $./\$
10	3, 4, 5, 9	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
11		simp1 996	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	6, 8	latmcl 15808	. . . . . 6 $/\$ $/\$ $./\$
13	3, 4, 5, 12	syl3anc 1228	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
14		dihglblem5a.h	. . . . . 6
15		dihglblem5a.i	. . . . . 6
16	6, 7, 14, 15	dihord 37092	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17	11, 13, 4, 16	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
18	10, 17	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
19	6, 7, 8	latmle2 15833	. . . . 5 $/\$ $/\$ $./\$
20	3, 4, 5, 19	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
21	6, 7, 14, 15	dihord 37092	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
22	11, 13, 5, 21	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
23	20, 22	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
24	18, 23	ssind 3718	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
25	14, 15	dihvalrel 37107	. . . . 5 $/\$
26		relin1 5129	. . . . 5
27	25, 26	syl 16	. . . 4 $/\$
28	27	3ad2ant1 1017	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
29		elin 3683	. . . 4 $/\$
30		dihglblem5a.j	. . . . . . 7 $.\/$
31		dihglblem5a.a	. . . . . . 7
32	6, 7, 30, 8, 31, 14	lhpmcvr2 35849	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	32	3adant3 1016	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34		simpl1 999	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35		simpl2 1000	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
36		simprl 756	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simprrl 765	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
38	36, 37	jca 532	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
39		simprrr 766	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40		dihglblem5a.p	. . . . . . . . 9
41		dihglblem5a.t	. . . . . . . . 9
42		dihglblem5a.r	. . . . . . . . 9
43		dihglblem5a.e	. . . . . . . . 9
44		dihglblem5a.g	. . . . . . . . 9
45		vex 3112	. . . . . . . . 9
46		vex 3112	. . . . . . . . 9
47	6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46	dihopelvalc 37077	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48	34, 35, 38, 39, 47	syl112anc 1232	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49		simpr 461	. . . . . . 7 $/\$ $/\$
50	48, 49	syl6bi 228	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		simpl3 1001	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
52		dihglblem5a.o	. . . . . . . . 9
53	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 37066	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
54	34, 51, 53	syl2anc 661	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
55	54	biimpd 207	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simprll 763	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3ad2ant3 1019	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
58		simp3rr 1070	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
59	58	fveq1d 5874	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
60		simp11 1026	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	7, 31, 14, 40	lhpocnel2 35844	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	60, 61	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2l 1022	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
64		simp2rl 1065	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
65	7, 31, 14, 41, 44	ltrniotacl 36406	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 62, 63, 64, 65	syl112anc 1232	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
67	52, 6	tendo02 36614	. . . . . . . . . . . . . . . . . 18
68	66, 67	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
69	59, 68	eqtrd 2498	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
70	69	cnveqd 5188	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
71		cnvresid 5664	. . . . . . . . . . . . . . 15
72	70, 71	syl6eq 2514	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
73	72	coeq2d 5175	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
74	6, 14, 41	ltrn1o 35949	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	60, 57, 74	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
76		f1of 5822	. . . . . . . . . . . . . 14
77		fcoi1 5765	. . . . . . . . . . . . . 14
78	75, 76, 77	3syl 20	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
79	73, 78	eqtrd 2498	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
80	79	fveq2d 5876	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
81		simp3l 1024	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqbrtrrd 4478	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
83		simprlr 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	83	3ad2ant3 1019	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
85		simp11l 1107	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
86	85, 2	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
87	6, 14, 41, 42	trlcl 35990	. . . . . . . . . . . 12 $/\$ $/\$
88	60, 57, 87	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
89		simp12l 1109	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
90		simp13l 1111	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
91	6, 7, 8	latlem12 15834	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $./\$
92	86, 88, 89, 90, 91	syl13anc 1230	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
93	82, 84, 92	mpbi2and 921	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
94	57, 93	jca 532	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
95	86, 89, 90, 12	syl3anc 1228	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
96		simp11r 1108	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
97	6, 14	lhpbase 35823	. . . . . . . . . . 11
98	96, 97	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
99	86, 89, 90, 19	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
100		simp13r 1112	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
101	6, 7, 86, 95, 90, 98, 99, 100	lattrd 15814	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
102	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 37066	. . . . . . . . 9 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$ $/\$ $./\$ $/\$
103	60, 95, 101, 102	syl12anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$
104	94, 58, 103	mpbir2and 922	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
105	104	3expia 1198	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $./\$
106	50, 55, 105	syl2and 483	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
107	33, 106	rexlimddv 2953	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
108	29, 107	syl5bi 217	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
109	28, 108	relssdv 5104	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
110	24, 109	eqssd 3516	1 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wrex 2808

cin 3470

wss 3471

cop 4038 class class class wbr 4456

cmpt 4515

cid 4799

ccnv 5007

cres 5010

ccom 5012

wrel 5013

wf 5590

wf1o 5593

cfv 5594

crio 6257 (class class class)co 6296

cbs 14643

cple 14718

coc 14719

cjn 15699

cmee 15700

clat 15801

catm 35089

chlt 35176

clh 35809

cltrn 35926

ctrl 35984

ctendo 36579

cdih 37056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-riotaBAD 34785

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-tpos 6973 df-undef 7020 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-n0 10817 df-z 10886 df-uz 11107 df-fz 11698 df-struct 14645 df-ndx 14646 df-slot 14647 df-base 14648 df-sets 14649 df-ress 14650 df-plusg 14724 df-mulr 14725 df-sca 14727 df-vsca 14728 df-0g 14858 df-preset 15683 df-poset 15701 df-plt 15714 df-lub 15730 df-glb 15731 df-join 15732 df-meet 15733 df-p0 15795 df-p1 15796 df-lat 15802 df-clat 15864 df-mgm 15998 df-sgrp 16037 df-mnd 16047 df-submnd 16093 df-grp 16183 df-minusg 16184 df-sbg 16185 df-subg 16324 df-cntz 16481 df-lsm 16782 df-cmn 16926 df-abl 16927 df-mgp 17268 df-ur 17280 df-ring 17326 df-oppr 17398 df-dvdsr 17416 df-unit 17417 df-invr 17447 df-dvr 17458 df-drng 17524 df-lmod 17640 df-lss 17705 df-lsp 17744 df-lvec 17875 df-oposet 35002 df-ol 35004 df-oml 35005 df-covers 35092 df-ats 35093 df-atl 35124 df-cvlat 35148 df-hlat 35177 df-llines 35323 df-lplanes 35324 df-lvols 35325 df-lines 35326 df-psubsp 35328 df-pmap 35329 df-padd 35621 df-lhyp 35813 df-laut 35814 df-ldil 35929 df-ltrn 35930 df-trl 35985 df-tendo 36582 df-edring 36584 df-disoa 36857 df-dvech 36907 df-dib 36967 df-dic 37001 df-dih 37057

This theorem is referenced by: dihmeetbN 37131

W3C validator