Theorem lautj 41130

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 2761	. 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 18606	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
8	7	3adant3r1 1201	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵)
9		lautj.i	. . . 4 ⊢ 𝐼 = (LAut‘𝐾)
10	1, 9	lautcl 41124	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
11	5, 8, 10	syl2anc 596	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) ∈ 𝐵)
12		simpr2 1214	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
13	1, 9	lautcl 41124	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
14	5, 12, 13	syl2anc 596	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋) ∈ 𝐵)
15		simpr3 1215	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
16	1, 9	lautcl 41124	. . . 4 ⊢ (((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) ∧ 𝑌 ∈ 𝐵) → (𝐹‘𝑌) ∈ 𝐵)
17	5, 15, 16	syl2anc 596	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌) ∈ 𝐵)
18	1, 6	latjcl 18606	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
19	3, 14, 17, 18	syl3anc 1398	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵)
20	1, 9	laut1o 41122	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵)
21	20	3ad2antr1 1207	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝐵)
22		f1ocnvfv1 7282	. . . . 5 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
23	21, 8, 22	syl2anc 596	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌))
24	1, 2, 6	latlej1 18615	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
25	3, 14, 17, 24	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
26		f1ocnvfv2 7283	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
27	21, 19, 26	syl2anc 596	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
28	25, 27	breqtrrd 5133	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑋)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
29		f1ocnvdm 7291	. . . . . . . 8 ⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ ((𝐹‘𝑋) ∨ (𝐹‘𝑌)) ∈ 𝐵) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
30	21, 19, 29	syl2anc 596	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))) ∈ 𝐵)
31	1, 2, 9	lautle 41121	. . . . . . 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 18616	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ (𝐹‘𝑌) ∈ 𝐵) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
35	3, 14, 17, 34	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)((𝐹‘𝑋) ∨ (𝐹‘𝑌)))
36	35, 27	breqtrrd 5133	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘𝑌)(le‘𝐾)(𝐹‘(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌)))))
37	1, 2, 9	lautle 41121	. . . . . . 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 18617	. . . . . 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 5127	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (◡𝐹‘(𝐹‘(𝑋 ∨ 𝑌)))(le‘𝐾)(◡𝐹‘((𝐹‘𝑋) ∨ (𝐹‘𝑌))))
44	1, 2, 9	lautcnvle 41126	. . . 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 18615	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
48	47	3adant3r1 1201	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌))
49	1, 2, 9	lautle 41121	. . . . 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 18616	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
53	52	3adant3r1 1201	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌))
54	1, 2, 9	lautle 41121	. . . . 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 18617	. . . 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 18612	1 ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ^◡ccnv 5650  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418  Basecbs 17380  lecple 17428  joincjn 18478  Latclat 18598  LAutclaut 41022

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-map 8842  df-proset 18461  df-poset 18480  df-lub 18511  df-glb 18512  df-join 18513  df-meet 18514  df-lat 18599  df-laut 41026

This theorem is used by:  ltrnj  41169