Theorem paddunN 33890

Description: The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 5798.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
paddun.a	|- A = ( Atoms ` K )
paddun.p	|- .+ = ( +P ` K )
paddun.o	|- ._|_ = ( _|_P ` K )

Assertion

Ref	Expression
paddunN	|- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )

Proof of Theorem paddunN

Step	Hyp	Ref	Expression
1		simp1 988	. . 3 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. HL )
2		paddun.a	. . . 4 |- A = ( Atoms ` K )
3		paddun.p	. . . 4 |- .+ = ( +P ` K )
4	2, 3	paddssat 33777	. . 3 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ A )
5	2, 3	paddunssN 33771	. . 3 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( S .+ T ) )
6		paddun.o	. . . 4 |- ._|_ = ( _|_P ` K )
7	2, 6	polcon3N 33880	. . 3 |- ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ ( S .+ T ) ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) )
8	1, 4, 5, 7	syl3anc 1219	. 2 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) C_ ( ._|_ ` ( S u. T ) ) )
9		hlclat 33322	. . . . . . 7 |- ( K e. HL -> K e. CLat )
10	9	3ad2ant1 1009	. . . . . 6 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. CLat )
11		unss 3633	. . . . . . . . . . 11 |- ( ( S C_ A /\ T C_ A ) <-> ( S u. T ) C_ A )
12	11	biimpi 194	. . . . . . . . . 10 |- ( ( S C_ A /\ T C_ A ) -> ( S u. T ) C_ A )
13	12	3adant1 1006	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ A )
14		eqid 2452	. . . . . . . . . 10 |- ( Base ` K ) = ( Base ` K )
15	14, 2	atssbase 33254	. . . . . . . . 9 |- A C_ ( Base ` K )
16	13, 15	syl6ss 3471	. . . . . . . 8 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S u. T ) C_ ( Base ` K ) )
17		eqid 2452	. . . . . . . . 9 |- ( lub ` K ) = ( lub ` K )
18	14, 17	clatlubcl 15396	. . . . . . . 8 |- ( ( K e. CLat /\ ( S u. T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) )
19	10, 16, 18	syl2anc 661	. . . . . . 7 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) )
20		eqid 2452	. . . . . . . 8 |- ( pmap ` K ) = ( pmap ` K )
21	14, 20	pmapssbaN 33723	. . . . . . 7 |- ( ( K e. HL /\ ( ( lub ` K ) ` ( S u. T ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) )
22	1, 19, 21	syl2anc 661	. . . . . 6 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) )
23	2, 6	polssatN 33871	. . . . . . . . . . . . 13 |- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` S ) C_ A )
24	23	3adant3 1008	. . . . . . . . . . . 12 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` S ) C_ A )
25	2, 6	polssatN 33871	. . . . . . . . . . . 12 |- ( ( K e. HL /\ ( ._|_ ` S ) C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A )
26	1, 24, 25	syl2anc 661	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ A )
27	2, 6	polssatN 33871	. . . . . . . . . . . . 13 |- ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` T ) C_ A )
28	27	3adant2 1007	. . . . . . . . . . . 12 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` T ) C_ A )
29	2, 6	polssatN 33871	. . . . . . . . . . . 12 |- ( ( K e. HL /\ ( ._|_ ` T ) C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A )
30	1, 28, 29	syl2anc 661	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) C_ A )
31	1, 26, 30	3jca 1168	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) )
32	2, 6	2polssN 33878	. . . . . . . . . . . 12 |- ( ( K e. HL /\ S C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
33	32	3adant3 1008	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )
34	2, 6	2polssN 33878	. . . . . . . . . . . 12 |- ( ( K e. HL /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
35	34	3adant2 1007	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( ._|_ ` ( ._|_ ` T ) ) )
36	33, 35	jca 532	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) )
37	2, 3	paddss12 33782	. . . . . . . . . 10 |- ( ( K e. HL /\ ( ._|_ ` ( ._|_ ` S ) ) C_ A /\ ( ._|_ ` ( ._|_ ` T ) ) C_ A ) -> ( ( S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ T C_ ( ._|_ ` ( ._|_ ` T ) ) ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) ) )
38	31, 36, 37	sylc 60	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) )
39	17, 2, 20, 6	2polvalN 33877	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) )
40	39	3adant3 1008	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` S ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) )
41	17, 2, 20, 6	2polvalN 33877	. . . . . . . . . . 11 |- ( ( K e. HL /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) )
42	41	3adant2 1007	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` T ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) )
43	40, 42	oveq12d 6213	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` S ) ) .+ ( ._|_ ` ( ._|_ ` T ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) )
44	38, 43	sseqtrd 3495	. . . . . . . 8 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) )
45		hllat 33327	. . . . . . . . . 10 |- ( K e. HL -> K e. Lat )
46	45	3ad2ant1 1009	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> K e. Lat )
47		simp2 989	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ A )
48	47, 15	syl6ss 3471	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> S C_ ( Base ` K ) )
49	14, 17	clatlubcl 15396	. . . . . . . . . 10 |- ( ( K e. CLat /\ S C_ ( Base ` K ) ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
50	10, 48, 49	syl2anc 661	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` S ) e. ( Base ` K ) )
51		simp3 990	. . . . . . . . . . 11 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ A )
52	51, 15	syl6ss 3471	. . . . . . . . . 10 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> T C_ ( Base ` K ) )
53	14, 17	clatlubcl 15396	. . . . . . . . . 10 |- ( ( K e. CLat /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
54	10, 52, 53	syl2anc 661	. . . . . . . . 9 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` T ) e. ( Base ` K ) )
55		eqid 2452	. . . . . . . . . 10 |- ( join ` K ) = ( join ` K )
56	14, 55, 20, 3	pmapjoin 33815	. . . . . . . . 9 |- ( ( K e. Lat /\ ( ( lub ` K ) ` S ) e. ( Base ` K ) /\ ( ( lub ` K ) ` T ) e. ( Base ` K ) ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
57	46, 50, 54, 56	syl3anc 1219	. . . . . . . 8 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` S ) ) .+ ( ( pmap ` K ) ` ( ( lub ` K ) ` T ) ) ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
58	44, 57	sstrd 3469	. . . . . . 7 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
59	14, 55, 17	lubun 15407	. . . . . . . . 9 |- ( ( K e. CLat /\ S C_ ( Base ` K ) /\ T C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) )
60	10, 48, 52, 59	syl3anc 1219	. . . . . . . 8 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S u. T ) ) = ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) )
61	60	fveq2d 5798	. . . . . . 7 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( ( lub ` K ) ` S ) ( join ` K ) ( ( lub ` K ) ` T ) ) ) )
62	58, 61	sseqtr4d 3496	. . . . . 6 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
63		eqid 2452	. . . . . . 7 |- ( le ` K ) = ( le ` K )
64	14, 63, 17	lubss 15405	. . . . . 6 |- ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) /\ ( S .+ T ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
65	10, 22, 62, 64	syl3anc 1219	. . . . 5 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) )
66	4, 15	syl6ss 3471	. . . . . . 7 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( S .+ T ) C_ ( Base ` K ) )
67	14, 17	clatlubcl 15396	. . . . . . 7 |- ( ( K e. CLat /\ ( S .+ T ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) )
68	10, 66, 67	syl2anc 661	. . . . . 6 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) )
69	14, 17	clatlubcl 15396	. . . . . . 7 |- ( ( K e. CLat /\ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) C_ ( Base ` K ) ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) )
70	10, 22, 69	syl2anc 661	. . . . . 6 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) )
71	14, 63, 20	pmaple 33724	. . . . . 6 |- ( ( K e. HL /\ ( ( lub ` K ) ` ( S .+ T ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) )
72	1, 68, 70, 71	syl3anc 1219	. . . . 5 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ( lub ` K ) ` ( S .+ T ) ) ( le ` K ) ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) <-> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) ) )
73	65, 72	mpbid 210	. . . 4 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) C_ ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) )
74	17, 2, 20, 6	2polvalN 33877	. . . . 5 |- ( ( K e. HL /\ ( S .+ T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) )
75	1, 4, 74	syl2anc 661	. . . 4 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S .+ T ) ) ) )
76	17, 2, 20, 6	2polvalN 33877	. . . . . 6 |- ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
77	1, 13, 76	syl2anc 661	. . . . 5 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
78	17, 2, 20	2pmaplubN 33889	. . . . . 6 |- ( ( K e. HL /\ ( S u. T ) C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
79	1, 13, 78	syl2anc 661	. . . . 5 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) )
80	77, 79	eqtr4d 2496	. . . 4 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` ( ( pmap ` K ) ` ( ( lub ` K ) ` ( S u. T ) ) ) ) ) )
81	73, 75, 80	3sstr4d 3502	. . 3 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) )
82	2, 6	2polcon4bN 33881	. . . 4 |- ( ( K e. HL /\ ( S .+ T ) C_ A /\ ( S u. T ) C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) )
83	1, 4, 13, 82	syl3anc 1219	. . 3 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ( ._|_ ` ( ._|_ ` ( S .+ T ) ) ) C_ ( ._|_ ` ( ._|_ ` ( S u. T ) ) ) <-> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) ) )
84	81, 83	mpbid 210	. 2 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S u. T ) ) C_ ( ._|_ ` ( S .+ T ) ) )
85	8, 84	eqssd 3476	1 |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   u. cun 3429   C_ wss 3431   class class class wbr 4395   ` cfv 5521  (class class class)co 6195   Basecbs 14287   lecple 14359   lubclub 15226   joincjn 15228   Latclat 15329   CLatccla 15391   Atomscatm 33227   HLchlt 33314   pmapcpmap 33460   +Pcpadd 33758   _|_PcpolN 33865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477  ax-riotaBAD 32923

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-nel 2648  df-ral 2801  df-rex 2802  df-reu 2803  df-rmo 2804  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-iun 4276  df-iin 4277  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-riota 6156  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-1st 6682  df-2nd 6683  df-undef 6897  df-poset 15230  df-plt 15242  df-lub 15258  df-glb 15259  df-join 15260  df-meet 15261  df-p0 15323  df-p1 15324  df-lat 15330  df-clat 15392  df-oposet 33140  df-ol 33142  df-oml 33143  df-covers 33230  df-ats 33231  df-atl 33262  df-cvlat 33286  df-hlat 33315  df-psubsp 33466  df-pmap 33467  df-padd 33759  df-polarityN 33866

This theorem is referenced by:  poldmj1N  33891