dihmeetlem1N - Mathbox for Norm Megill

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

Theorem dihmeetlem1N 34929

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 1054	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
2		hllat 33000	. . . . . 6
3	1, 2	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp2l 1056	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp3l 1058	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
6		dihglblem5a.b	. . . . . 6
7		dihglblem5a.l	. . . . . 6
8		dihglblem5a.m	. . . . . 6 $./\$
9	6, 7, 8	latmle1 16400	. . . . 5 $/\$ $/\$ $./\$
10	3, 4, 5, 9	syl3anc 1292	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
11		simp1 1030	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	6, 8	latmcl 16376	. . . . . 6 $/\$ $/\$ $./\$
13	3, 4, 5, 12	syl3anc 1292	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
14		dihglblem5a.h	. . . . . 6
15		dihglblem5a.i	. . . . . 6
16	6, 7, 14, 15	dihord 34903	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17	11, 13, 4, 16	syl3anc 1292	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
18	10, 17	mpbird 240	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
19	6, 7, 8	latmle2 16401	. . . . 5 $/\$ $/\$ $./\$
20	3, 4, 5, 19	syl3anc 1292	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
21	6, 7, 14, 15	dihord 34903	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
22	11, 13, 5, 21	syl3anc 1292	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
23	20, 22	mpbird 240	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
24	18, 23	ssind 3647	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
25	14, 15	dihvalrel 34918	. . . . 5 $/\$
26		relin1 4956	. . . . 5
27	25, 26	syl 17	. . . 4 $/\$
28	27	3ad2ant1 1051	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
29		elin 3608	. . . 4 $/\$
30		dihglblem5a.j	. . . . . . 7 $.\/$
31		dihglblem5a.a	. . . . . . 7
32	6, 7, 30, 8, 31, 14	lhpmcvr2 33660	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	32	3adant3 1050	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34		simpl1 1033	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35		simpl2 1034	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
36		simprl 772	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simprrl 782	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
38	36, 37	jca 541	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
39		simprrr 783	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40		dihglblem5a.p	. . . . . . . . 9
41		dihglblem5a.t	. . . . . . . . 9
42		dihglblem5a.r	. . . . . . . . 9
43		dihglblem5a.e	. . . . . . . . 9
44		dihglblem5a.g	. . . . . . . . 9
45		vex 3034	. . . . . . . . 9
46		vex 3034	. . . . . . . . 9
47	6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46	dihopelvalc 34888	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48	34, 35, 38, 39, 47	syl112anc 1296	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49		simpr 468	. . . . . . 7 $/\$ $/\$
50	48, 49	syl6bi 236	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		simpl3 1035	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
52		dihglblem5a.o	. . . . . . . . 9
53	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34877	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
54	34, 51, 53	syl2anc 673	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
55	54	biimpd 212	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simprll 780	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3ad2ant3 1053	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
58		simp3rr 1104	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
59	58	fveq1d 5881	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
60		simp11 1060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	7, 31, 14, 40	lhpocnel2 33655	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2l 1056	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
64		simp2rl 1099	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
65	7, 31, 14, 41, 44	ltrniotacl 34217	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 62, 63, 64, 65	syl112anc 1296	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
67	52, 6	tendo02 34425	. . . . . . . . . . . . . . . . . 18
68	66, 67	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
69	59, 68	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
70	69	cnveqd 5015	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
71		cnvresid 5663	. . . . . . . . . . . . . . 15
72	70, 71	syl6eq 2521	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
73	72	coeq2d 5002	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
74	6, 14, 41	ltrn1o 33760	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	60, 57, 74	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
76		f1of 5828	. . . . . . . . . . . . . 14
77		fcoi1 5769	. . . . . . . . . . . . . 14
78	75, 76, 77	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
79	73, 78	eqtrd 2505	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
80	79	fveq2d 5883	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
81		simp3l 1058	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqbrtrrd 4418	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
83		simprlr 781	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	83	3ad2ant3 1053	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
85		simp11l 1141	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
86	85, 2	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
87	6, 14, 41, 42	trlcl 33801	. . . . . . . . . . . 12 $/\$ $/\$
88	60, 57, 87	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
89		simp12l 1143	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
90		simp13l 1145	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
91	6, 7, 8	latlem12 16402	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $./\$
92	86, 88, 89, 90, 91	syl13anc 1294	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
93	82, 84, 92	mpbi2and 935	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
94	57, 93	jca 541	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
95	86, 89, 90, 12	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
96		simp11r 1142	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
97	6, 14	lhpbase 33634	. . . . . . . . . . 11
98	96, 97	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
99	86, 89, 90, 19	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
100		simp13r 1146	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
101	6, 7, 86, 95, 90, 98, 99, 100	lattrd 16382	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
102	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34877	. . . . . . . . 9 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$ $/\$ $./\$ $/\$
103	60, 95, 101, 102	syl12anc 1290	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$
104	94, 58, 103	mpbir2and 936	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
105	104	3expia 1233	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $./\$
106	50, 55, 105	syl2and 491	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
107	33, 106	rexlimddv 2875	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
108	29, 107	syl5bi 225	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
109	28, 108	relssdv 4932	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
110	24, 109	eqssd 3435	1 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wrex 2757

cin 3389

wss 3390

cop 3965 class class class wbr 4395

cmpt 4454

cid 4749

ccnv 4838

cres 4841

ccom 4843

wrel 4844

wf 5585

wf1o 5588

cfv 5589

crio 6269 (class class class)co 6308

cbs 15199

cple 15275

coc 15276

cjn 16267

cmee 16268

clat 16369

catm 32900

chlt 32987

clh 33620

cltrn 33737

ctrl 33795

ctendo 34390

cdih 34867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-riotaBAD 32589

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-tpos 6991 df-undef 7038 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-sca 15284 df-vsca 15285 df-0g 15418 df-preset 16251 df-poset 16269 df-plt 16282 df-lub 16298 df-glb 16299 df-join 16300 df-meet 16301 df-p0 16363 df-p1 16364 df-lat 16370 df-clat 16432 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-grp 16751 df-minusg 16752 df-sbg 16753 df-subg 16892 df-cntz 17049 df-lsm 17366 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-ring 17860 df-oppr 17929 df-dvdsr 17947 df-unit 17948 df-invr 17978 df-dvr 17989 df-drng 18055 df-lmod 18171 df-lss 18234 df-lsp 18273 df-lvec 18404 df-oposet 32813 df-ol 32815 df-oml 32816 df-covers 32903 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988 df-llines 33134 df-lplanes 33135 df-lvols 33136 df-lines 33137 df-psubsp 33139 df-pmap 33140 df-padd 33432 df-lhyp 33624 df-laut 33625 df-ldil 33740 df-ltrn 33741 df-trl 33796 df-tendo 34393 df-edring 34395 df-disoa 34668 df-dvech 34718 df-dib 34778 df-dic 34812 df-dih 34868

This theorem is referenced by: dihmeetbN 34942

W3C validator