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 34852

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 1031	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
2		hllat 32923	. . . . . 6
3	1, 2	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp2l 1033	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp3l 1035	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
6		dihglblem5a.b	. . . . . 6
7		dihglblem5a.l	. . . . . 6
8		dihglblem5a.m	. . . . . 6 $./\$
9	6, 7, 8	latmle1 16315	. . . . 5 $/\$ $/\$ $./\$
10	3, 4, 5, 9	syl3anc 1267	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
11		simp1 1007	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	6, 8	latmcl 16291	. . . . . 6 $/\$ $/\$ $./\$
13	3, 4, 5, 12	syl3anc 1267	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
14		dihglblem5a.h	. . . . . 6
15		dihglblem5a.i	. . . . . 6
16	6, 7, 14, 15	dihord 34826	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17	11, 13, 4, 16	syl3anc 1267	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
18	10, 17	mpbird 236	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
19	6, 7, 8	latmle2 16316	. . . . 5 $/\$ $/\$ $./\$
20	3, 4, 5, 19	syl3anc 1267	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
21	6, 7, 14, 15	dihord 34826	. . . . 5 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
22	11, 13, 5, 21	syl3anc 1267	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
23	20, 22	mpbird 236	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
24	18, 23	ssind 3655	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
25	14, 15	dihvalrel 34841	. . . . 5 $/\$
26		relin1 4950	. . . . 5
27	25, 26	syl 17	. . . 4 $/\$
28	27	3ad2ant1 1028	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
29		elin 3616	. . . 4 $/\$
30		dihglblem5a.j	. . . . . . 7 $.\/$
31		dihglblem5a.a	. . . . . . 7
32	6, 7, 30, 8, 31, 14	lhpmcvr2 33583	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	32	3adant3 1027	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34		simpl1 1010	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35		simpl2 1011	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
36		simprl 763	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
37		simprrl 773	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
38	36, 37	jca 535	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
39		simprrr 774	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40		dihglblem5a.p	. . . . . . . . 9
41		dihglblem5a.t	. . . . . . . . 9
42		dihglblem5a.r	. . . . . . . . 9
43		dihglblem5a.e	. . . . . . . . 9
44		dihglblem5a.g	. . . . . . . . 9
45		vex 3047	. . . . . . . . 9
46		vex 3047	. . . . . . . . 9
47	6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46	dihopelvalc 34811	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48	34, 35, 38, 39, 47	syl112anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
49		simpr 463	. . . . . . 7 $/\$ $/\$
50	48, 49	syl6bi 232	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
51		simpl3 1012	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
52		dihglblem5a.o	. . . . . . . . 9
53	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34800	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
54	34, 51, 53	syl2anc 666	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
55	54	biimpd 211	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simprll 771	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3ad2ant3 1030	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
58		simp3rr 1081	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
59	58	fveq1d 5865	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
60		simp11 1037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	7, 31, 14, 40	lhpocnel2 33578	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2l 1033	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
64		simp2rl 1076	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
65	7, 31, 14, 41, 44	ltrniotacl 34140	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 62, 63, 64, 65	syl112anc 1271	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
67	52, 6	tendo02 34348	. . . . . . . . . . . . . . . . . 18
68	66, 67	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
69	59, 68	eqtrd 2484	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
70	69	cnveqd 5009	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
71		cnvresid 5651	. . . . . . . . . . . . . . 15
72	70, 71	syl6eq 2500	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
73	72	coeq2d 4996	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
74	6, 14, 41	ltrn1o 33683	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	60, 57, 74	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
76		f1of 5812	. . . . . . . . . . . . . 14
77		fcoi1 5755	. . . . . . . . . . . . . 14
78	75, 76, 77	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
79	73, 78	eqtrd 2484	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
80	79	fveq2d 5867	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
81		simp3l 1035	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqbrtrrd 4424	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
83		simprlr 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	83	3ad2ant3 1030	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
85		simp11l 1118	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
86	85, 2	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
87	6, 14, 41, 42	trlcl 33724	. . . . . . . . . . . 12 $/\$ $/\$
88	60, 57, 87	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
89		simp12l 1120	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
90		simp13l 1122	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
91	6, 7, 8	latlem12 16317	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $./\$
92	86, 88, 89, 90, 91	syl13anc 1269	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
93	82, 84, 92	mpbi2and 931	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
94	57, 93	jca 535	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
95	86, 89, 90, 12	syl3anc 1267	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
96		simp11r 1119	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
97	6, 14	lhpbase 33557	. . . . . . . . . . 11
98	96, 97	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
99	86, 89, 90, 19	syl3anc 1267	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
100		simp13r 1123	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$
101	6, 7, 86, 95, 90, 98, 99, 100	lattrd 16297	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
102	6, 7, 14, 41, 42, 52, 15	dihopelvalbN 34800	. . . . . . . . 9 $/\$ $/\$ $./\$ $/\$ $./\$ $./\$ $/\$ $./\$ $/\$
103	60, 95, 101, 102	syl12anc 1265	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$
104	94, 58, 103	mpbir2and 932	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $./\$
105	104	3expia 1209	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $./\$
106	50, 55, 105	syl2and 486	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
107	33, 106	rexlimddv 2882	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
108	29, 107	syl5bi 221	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
109	28, 108	relssdv 4926	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$
110	24, 109	eqssd 3448	1 $/\$ $/\$ $/\$ $/\$ $/\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wrex 2737

cin 3402

wss 3403

cop 3973 class class class wbr 4401

cmpt 4460

cid 4743

ccnv 4832

cres 4835

ccom 4837

wrel 4838

wf 5577

wf1o 5580

cfv 5581

crio 6249 (class class class)co 6288

cbs 15114

cple 15190

coc 15191

cjn 16182

cmee 16183

clat 16284

catm 32823

chlt 32910

clh 33543

cltrn 33660

ctrl 33718

ctendo 34313

cdih 34790

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-riotaBAD 32519

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-iin 4280 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-tpos 6970 df-undef 7017 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-map 7471 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-5 10668 df-6 10669 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782 df-struct 15116 df-ndx 15117 df-slot 15118 df-base 15119 df-sets 15120 df-ress 15121 df-plusg 15196 df-mulr 15197 df-sca 15199 df-vsca 15200 df-0g 15333 df-preset 16166 df-poset 16184 df-plt 16197 df-lub 16213 df-glb 16214 df-join 16215 df-meet 16216 df-p0 16278 df-p1 16279 df-lat 16285 df-clat 16347 df-mgm 16481 df-sgrp 16520 df-mnd 16530 df-submnd 16576 df-grp 16666 df-minusg 16667 df-sbg 16668 df-subg 16807 df-cntz 16964 df-lsm 17281 df-cmn 17425 df-abl 17426 df-mgp 17717 df-ur 17729 df-ring 17775 df-oppr 17844 df-dvdsr 17862 df-unit 17863 df-invr 17893 df-dvr 17904 df-drng 17970 df-lmod 18086 df-lss 18149 df-lsp 18188 df-lvec 18319 df-oposet 32736 df-ol 32738 df-oml 32739 df-covers 32826 df-ats 32827 df-atl 32858 df-cvlat 32882 df-hlat 32911 df-llines 33057 df-lplanes 33058 df-lvols 33059 df-lines 33060 df-psubsp 33062 df-pmap 33063 df-padd 33355 df-lhyp 33547 df-laut 33548 df-ldil 33663 df-ltrn 33664 df-trl 33719 df-tendo 34316 df-edring 34318 df-disoa 34591 df-dvech 34641 df-dib 34701 df-dic 34735 df-dih 34791

This theorem is referenced by: dihmeetbN 34865

W3C validator