Theorem lautj 40598

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 2741	. 2 ⊢ (le‘𝐾) = (le‘𝐾)
3		simpl 484	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐾 ∈ Lat)
4		simpr1 1202	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹 ∈ 𝐼)
5	3, 4	jca 517	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼))
6		lautj.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7	1, 6	latjcl 18400	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	7	3adant3r1 1190	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵)
9		lautj.i	. . . 4 ⊢ 𝐼 = (LAut‘𝐾)
10	1, 9	lautcl 40592	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
11	5, 8, 10	syl2anc 591	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
12		simpr2 1203	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
13	1, 9	lautcl 40592	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
14	5, 12, 13	syl2anc 591	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝐵)
15		simpr3 1204	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
16	1, 9	lautcl 40592	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝐵)
17	5, 15, 16	syl2anc 591	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝐵)
18	1, 6	latjcl 18400	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
19	3, 14, 17, 18	syl3anc 1380	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
20	1, 9	laut1o 40590	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
21	20	3ad2antr1 1196	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝐵)
22		f1ocnvfv1 7223	. . . . 5 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
23	21, 8, 22	syl2anc 591	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
24	1, 2, 6	latlej1 18409	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
25	3, 14, 17, 24	syl3anc 1380	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
26		f1ocnvfv2 7224	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
27	21, 19, 26	syl2anc 591	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
28	25, 27	breqtrrd 5102	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
29		f1ocnvdm 7232	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
30	21, 19, 29	syl2anc 591	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
31	1, 2, 9	lautle 40589	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
32	5, 12, 30, 31	syl12anc 843	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
33	28, 32	mpbird 259	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
34	1, 2, 6	latlej2 18410	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
35	3, 14, 17, 34	syl3anc 1380	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
36	35, 27	breqtrrd 5102	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
37	1, 2, 9	lautle 40589	. . . . . . 7 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
38	5, 15, 30, 37	syl12anc 843	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))))
39	36, 38	mpbird 259	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
40	1, 2, 6	latjle12 18411	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
41	3, 12, 15, 30, 40	syl13anc 1381	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∧ 𝑌(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
42	33, 39, 41	mpbi2and 719	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
43	23, 42	eqbrtrd 5096	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
44	1, 2, 9	lautcnvle 40594	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ ((𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
45	5, 11, 19, 44	syl12anc 843	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ↔ (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
46	43, 45	mpbird 259	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌))(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
47	1, 2, 6	latlej1 18409	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
48	47	3adant3r1 1190	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
49	1, 2, 9	lautle 40589	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
50	5, 12, 8, 49	syl12anc 843	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
51	48, 50	mpbid 234	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
52	1, 2, 6	latlej2 18410	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
53	52	3adant3r1 1190	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
54	1, 2, 9	lautle 40589	. . . . 5 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
55	5, 15, 8, 54	syl12anc 843	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑌(le‘𝐾)(𝑋 ∨ 𝑌) ↔ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
56	53, 55	mpbid 234	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
57	1, 2, 6	latjle12 18411	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
58	3, 14, 17, 11, 57	syl13anc 1381	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝐹‘𝑋)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)) ∧ (𝐹‘𝑌)(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))) ↔ ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌))))
59	51, 56, 58	mpbi2and 719	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌))(le‘𝐾)(𝐹‘(𝑋 ∨ 𝑌)))
60	1, 2, 3, 11, 19, 46, 59	latasymd 18406	1 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   class class class wbr 5074  ^◡ccnv 5619  –1-1-onto→wf1o 6487  ‘cfv 6488  (class class class)co 7359  Basecbs 17174  lecple 17222  joincjn 18272  Latclat 18392  LAutclaut 40490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-map 8769  df-proset 18255  df-poset 18274  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18393  df-laut 40494

This theorem is referenced by:  ltrnj  40637