Theorem lautj 40050

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 2740	. 2 ⊢ (le‘𝐾) = (le‘𝐾)
3		simpl 482	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ Lat)
4		simpr1 1194	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹 ∈ 𝐼)
5	3, 4	jca 511	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼))
6		lautj.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7	1, 6	latjcl 18509	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	7	3adant3r1 1182	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵)
9		lautj.i	. . . 4 ⊢ 𝐼 = (LAut‘𝐾)
10	1, 9	lautcl 40044	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
11	5, 8, 10	syl2anc 583	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
12		simpr2 1195	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
13	1, 9	lautcl 40044	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
14	5, 12, 13	syl2anc 583	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝐵)
15		simpr3 1196	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
16	1, 9	lautcl 40044	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝐵)
17	5, 15, 16	syl2anc 583	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝐵)
18	1, 6	latjcl 18509	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
19	3, 14, 17, 18	syl3anc 1371	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
20	1, 9	laut1o 40042	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
21	20	3ad2antr1 1188	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝐵)
22		f1ocnvfv1 7312	. . . . 5 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
23	21, 8, 22	syl2anc 583	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
24	1, 2, 6	latlej1 18518	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
25	3, 14, 17, 24	syl3anc 1371	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
26		f1ocnvfv2 7313	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
27	21, 19, 26	syl2anc 583	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
28	25, 27	breqtrrd 5194	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
29		f1ocnvdm 7321	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
30	21, 19, 29	syl2anc 583	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
31	1, 2, 9	lautle 40041	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
32	5, 12, 30, 31	syl12anc 836	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
33	28, 32	mpbird 257	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
34	1, 2, 6	latlej2 18519	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
35	3, 14, 17, 34	syl3anc 1371	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
36	35, 27	breqtrrd 5194	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
37	1, 2, 9	lautle 40041	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
38	5, 15, 30, 37	syl12anc 836	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
39	36, 38	mpbird 257	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
40	1, 2, 6	latjle12 18520	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
41	3, 12, 15, 30, 40	syl13anc 1372	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
42	33, 39, 41	mpbi2and 711	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
43	23, 42	eqbrtrd 5188	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
44	1, 2, 9	lautcnvle 40046	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ ((𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
45	5, 11, 19, 44	syl12anc 836	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
46	43, 45	mpbird 257	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
47	1, 2, 6	latlej1 18518	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
48	47	3adant3r1 1182	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
49	1, 2, 9	lautle 40041	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
50	5, 12, 8, 49	syl12anc 836	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
51	48, 50	mpbid 232	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
52	1, 2, 6	latlej2 18519	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
53	52	3adant3r1 1182	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
54	1, 2, 9	lautle 40041	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
55	5, 15, 8, 54	syl12anc 836	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
56	53, 55	mpbid 232	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
57	1, 2, 6	latjle12 18520	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
58	3, 14, 17, 11, 57	syl13anc 1372	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
59	51, 56, 58	mpbi2and 711	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
60	1, 2, 3, 11, 19, 46, 59	latasymd 18515	1 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ^◡ccnv 5699  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  lecple 17318  joincjn 18381  Latclat 18501  LAutclaut 39942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-map 8886  df-proset 18365  df-poset 18383  df-lub 18416  df-glb 18417  df-join 18418  df-meet 18419  df-lat 18502  df-laut 39946

This theorem is referenced by:  ltrnj  40089