Theorem lautj 38556

Description: Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.)

Hypotheses

Ref	Expression
lautj.b	⊢ 𝐵 = (Base‘𝐾)
lautj.j	⊢ ∨ = (join‘𝐾)
lautj.i	⊢ 𝐼 = (LAut‘𝐾)

Assertion

Ref	Expression
lautj	⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

Proof of Theorem lautj

Step	Hyp	Ref	Expression
1		lautj.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2736	. 2 ⊢ (le‘𝐾) = (le‘𝐾)
3		simpl 483	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ Lat)
4		simpr1 1194	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹 ∈ 𝐼)
5	3, 4	jca 512	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼))
6		lautj.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7	1, 6	latjcl 18328	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	7	3adant3r1 1182	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵)
9		lautj.i	. . . 4 ⊢ 𝐼 = (LAut‘𝐾)
10	1, 9	lautcl 38550	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
11	5, 8, 10	syl2anc 584	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
12		simpr2 1195	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
13	1, 9	lautcl 38550	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
14	5, 12, 13	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝐵)
15		simpr3 1196	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
16	1, 9	lautcl 38550	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝐵)
17	5, 15, 16	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝐵)
18	1, 6	latjcl 18328	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
19	3, 14, 17, 18	syl3anc 1371	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
20	1, 9	laut1o 38548	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
21	20	3ad2antr1 1188	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝐵)
22		f1ocnvfv1 7222	. . . . 5 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
23	21, 8, 22	syl2anc 584	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
24	1, 2, 6	latlej1 18337	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
25	3, 14, 17, 24	syl3anc 1371	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
26		f1ocnvfv2 7223	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
27	21, 19, 26	syl2anc 584	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
28	25, 27	breqtrrd 5133	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
29		f1ocnvdm 7231	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
30	21, 19, 29	syl2anc 584	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
31	1, 2, 9	lautle 38547	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
32	5, 12, 30, 31	syl12anc 835	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
33	28, 32	mpbird 256	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
34	1, 2, 6	latlej2 18338	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
35	3, 14, 17, 34	syl3anc 1371	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
36	35, 27	breqtrrd 5133	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
37	1, 2, 9	lautle 38547	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
38	5, 15, 30, 37	syl12anc 835	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
39	36, 38	mpbird 256	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
40	1, 2, 6	latjle12 18339	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
41	3, 12, 15, 30, 40	syl13anc 1372	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
42	33, 39, 41	mpbi2and 710	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
43	23, 42	eqbrtrd 5127	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
44	1, 2, 9	lautcnvle 38552	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ ((𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
45	5, 11, 19, 44	syl12anc 835	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
46	43, 45	mpbird 256	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
47	1, 2, 6	latlej1 18337	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
48	47	3adant3r1 1182	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
49	1, 2, 9	lautle 38547	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
50	5, 12, 8, 49	syl12anc 835	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
51	48, 50	mpbid 231	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
52	1, 2, 6	latlej2 18338	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
53	52	3adant3r1 1182	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
54	1, 2, 9	lautle 38547	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
55	5, 15, 8, 54	syl12anc 835	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
56	53, 55	mpbid 231	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
57	1, 2, 6	latjle12 18339	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
58	3, 14, 17, 11, 57	syl13anc 1372	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
59	51, 56, 58	mpbi2and 710	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
60	1, 2, 3, 11, 19, 46, 59	latasymd 18334	1 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   class class class wbr 5105  ^◡ccnv 5632  –1-1-onto→wf1o 6495  ‘cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  joincjn 18200  Latclat 18320  LAutclaut 38448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-proset 18184  df-poset 18202  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-lat 18321  df-laut 38452

This theorem is referenced by:  ltrnj  38595