Theorem lautj 40925

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 2765	. 2 ⊢ (le‘𝐾) = (le‘𝐾)
3		simpl 488	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ Lat)
4		simpr1 1213	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹 ∈ 𝐼)
5	3, 4	jca 521	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼))
6		lautj.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7	1, 6	latjcl 18517	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	7	3adant3r1 1201	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵)
9		lautj.i	. . . 4 ⊢ 𝐼 = (LAut‘𝐾)
10	1, 9	lautcl 40919	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
11	5, 8, 10	syl2anc 596	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
12		simpr2 1214	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
13	1, 9	lautcl 40919	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
14	5, 12, 13	syl2anc 596	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝐵)
15		simpr3 1215	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
16	1, 9	lautcl 40919	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝐵)
17	5, 15, 16	syl2anc 596	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝐵)
18	1, 6	latjcl 18517	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
19	3, 14, 17, 18	syl3anc 1398	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
20	1, 9	laut1o 40917	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
21	20	3ad2antr1 1207	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝐵)
22		f1ocnvfv1 7283	. . . . 5 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
23	21, 8, 22	syl2anc 596	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
24	1, 2, 6	latlej1 18526	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
25	3, 14, 17, 24	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
26		f1ocnvfv2 7284	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
27	21, 19, 26	syl2anc 596	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
28	25, 27	breqtrrd 5141	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
29		f1ocnvdm 7292	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
30	21, 19, 29	syl2anc 596	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
31	1, 2, 9	lautle 40916	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
32	5, 12, 30, 31	syl12anc 850	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
33	28, 32	mpbird 260	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
34	1, 2, 6	latlej2 18527	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
35	3, 14, 17, 34	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
36	35, 27	breqtrrd 5141	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
37	1, 2, 9	lautle 40916	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
38	5, 15, 30, 37	syl12anc 850	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
39	36, 38	mpbird 260	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
40	1, 2, 6	latjle12 18528	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
41	3, 12, 15, 30, 40	syl13anc 1399	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
42	33, 39, 41	mpbi2and 725	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
43	23, 42	eqbrtrd 5135	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
44	1, 2, 9	lautcnvle 40921	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ ((𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
45	5, 11, 19, 44	syl12anc 850	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
46	43, 45	mpbird 260	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
47	1, 2, 6	latlej1 18526	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
48	47	3adant3r1 1201	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
49	1, 2, 9	lautle 40916	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
50	5, 12, 8, 49	syl12anc 850	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
51	48, 50	mpbid 235	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
52	1, 2, 6	latlej2 18527	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
53	52	3adant3r1 1201	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
54	1, 2, 9	lautle 40916	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
55	5, 15, 8, 54	syl12anc 850	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
56	53, 55	mpbid 235	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
57	1, 2, 6	latjle12 18528	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
58	3, 14, 17, 11, 57	syl13anc 1399	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
59	51, 56, 58	mpbi2and 725	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
60	1, 2, 3, 11, 19, 46, 59	latasymd 18523	1 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   class class class wbr 5111  ^◡ccnv 5662  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7419  Basecbs 17291  lecple 17339  joincjn 18389  Latclat 18509  LAutclaut 40817

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-map 8832  df-proset 18372  df-poset 18391  df-lub 18422  df-glb 18423  df-join 18424  df-meet 18425  df-lat 18510  df-laut 40821

This theorem is used by:  ltrnj  40964