Theorem ordtbas2 21216

Description: Lemma for ordtbas 21217. (Contributed by Mario Carneiro, 3-Sep-2015.)

Hypotheses

Ref	Expression
ordtval.1	⊢ 𝑋 = dom 𝑅
ordtval.2	⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})
ordtval.3	⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})
ordtval.4	⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})

Assertion

Ref	Expression
ordtbas2	⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶))

Distinct variable groups:   𝑎,𝑏,𝐴   𝑥,𝑎,𝑦,𝑅,𝑏   𝑋,𝑎,𝑏,𝑥,𝑦   𝐵,𝑎,𝑏

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem ordtbas2

Dummy variables 𝑚 𝑛 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssun1 3927	. . . . . 6 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		ssun2 3928	. . . . . . 7 ⊢ (𝐴 ∪ 𝐵) ⊆ ({𝑋} ∪ (𝐴 ∪ 𝐵))
3		ordtval.1	. . . . . . . . . 10 ⊢ 𝑋 = dom 𝑅
4		ordtval.2	. . . . . . . . . 10 ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})
5		ordtval.3	. . . . . . . . . 10 ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})
6	3, 4, 5	ordtuni 21215	. . . . . . . . 9 ⊢ (𝑅 ∈ TosetRel → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵)))
7		dmexg 7248	. . . . . . . . . 10 ⊢ (𝑅 ∈ TosetRel → dom 𝑅 ∈ V)
8	3, 7	syl5eqel 2854	. . . . . . . . 9 ⊢ (𝑅 ∈ TosetRel → 𝑋 ∈ V)
9	6, 8	eqeltrrd 2851	. . . . . . . 8 ⊢ (𝑅 ∈ TosetRel → ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V)
10		uniexb 7124	. . . . . . . 8 ⊢ (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V ↔ ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V)
11	9, 10	sylibr 224	. . . . . . 7 ⊢ (𝑅 ∈ TosetRel → ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V)
12		ssexg 4939	. . . . . . 7 ⊢ (((𝐴 ∪ 𝐵) ⊆ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∧ ({𝑋} ∪ (𝐴 ∪ 𝐵)) ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
13	2, 11, 12	sylancr 575	. . . . . 6 ⊢ (𝑅 ∈ TosetRel → (𝐴 ∪ 𝐵) ∈ V)
14		ssexg 4939	. . . . . 6 ⊢ ((𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ∈ V) → 𝐴 ∈ V)
15	1, 13, 14	sylancr 575	. . . . 5 ⊢ (𝑅 ∈ TosetRel → 𝐴 ∈ V)
16		ssun2 3928	. . . . . 6 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
17		ssexg 4939	. . . . . 6 ⊢ ((𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ∈ V) → 𝐵 ∈ V)
18	16, 13, 17	sylancr 575	. . . . 5 ⊢ (𝑅 ∈ TosetRel → 𝐵 ∈ V)
19		elfiun 8496	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) ↔ (𝑧 ∈ (fi‘𝐴) ∨ 𝑧 ∈ (fi‘𝐵) ∨ ∃𝑚 ∈ (fi‘𝐴)∃𝑛 ∈ (fi‘𝐵)𝑧 = (𝑚 ∩ 𝑛))))
20	15, 18, 19	syl2anc 573	. . . 4 ⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) ↔ (𝑧 ∈ (fi‘𝐴) ∨ 𝑧 ∈ (fi‘𝐵) ∨ ∃𝑚 ∈ (fi‘𝐴)∃𝑛 ∈ (fi‘𝐵)𝑧 = (𝑚 ∩ 𝑛))))
21	3, 4	ordtbaslem 21213	. . . . . . . 8 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
22	21, 1	syl6eqss 3804	. . . . . . 7 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) ⊆ (𝐴 ∪ 𝐵))
23		ssun1 3927	. . . . . . 7 ⊢ (𝐴 ∪ 𝐵) ⊆ ((𝐴 ∪ 𝐵) ∪ 𝐶)
24	22, 23	syl6ss 3764	. . . . . 6 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) ⊆ ((𝐴 ∪ 𝐵) ∪ 𝐶))
25	24	sseld 3751	. . . . 5 ⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘𝐴) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
26		cnvtsr 17430	. . . . . . . . . 10 ⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel )
27		df-rn 5261	. . . . . . . . . . 11 ⊢ ran 𝑅 = dom ◡𝑅
28		eqid 2771	. . . . . . . . . . 11 ⊢ ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥})
29	27, 28	ordtbaslem 21213	. . . . . . . . . 10 ⊢ (◡𝑅 ∈ TosetRel → (fi‘ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥})) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}))
30	26, 29	syl 17	. . . . . . . . 9 ⊢ (𝑅 ∈ TosetRel → (fi‘ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥})) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}))
31		tsrps 17429	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel)
32	3	psrn 17417	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅)
33	31, 32	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ TosetRel → 𝑋 = ran 𝑅)
34		vex 3354	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
35		vex 3354	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
36	34, 35	brcnv 5442	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
37	36	bicomi 214	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑅𝑦 ↔ 𝑦◡𝑅𝑥)
38	37	notbii 309	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑦◡𝑅𝑥)
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ TosetRel → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑦◡𝑅𝑥))
40	33, 39	rabeqbidv 3345	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ TosetRel → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} = {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥})
41	33, 40	mpteq12dv 4868	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ TosetRel → (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) = (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}))
42	41	rneqd 5490	. . . . . . . . . . 11 ⊢ (𝑅 ∈ TosetRel → ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}))
43	5, 42	syl5eq 2817	. . . . . . . . . 10 ⊢ (𝑅 ∈ TosetRel → 𝐵 = ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥}))
44	43	fveq2d 6337	. . . . . . . . 9 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐵) = (fi‘ran (𝑥 ∈ ran 𝑅 ↦ {𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦◡𝑅𝑥})))
45	30, 44, 43	3eqtr4d 2815	. . . . . . . 8 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐵) = 𝐵)
46	45, 16	syl6eqss 3804	. . . . . . 7 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐵) ⊆ (𝐴 ∪ 𝐵))
47	46, 23	syl6ss 3764	. . . . . 6 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐵) ⊆ ((𝐴 ∪ 𝐵) ∪ 𝐶))
48	47	sseld 3751	. . . . 5 ⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘𝐵) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
49		ssun2 3928	. . . . . . . 8 ⊢ 𝐶 ⊆ ((𝐴 ∪ 𝐵) ∪ 𝐶)
50	21, 4	syl6eq 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}))
51	50	eleq2d 2836	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ TosetRel → (𝑚 ∈ (fi‘𝐴) ↔ 𝑚 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})))
52		vex 3354	. . . . . . . . . . . . . . 15 ⊢ 𝑚 ∈ V
53		breq2 4791	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑎))
54	53	notbid 307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦𝑅𝑎))
55	54	rabbidv 3339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎})
56	55	cbvmptv 4885	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑎 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎})
57	56	elrnmpt 5509	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ V → (𝑚 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}))
58	52, 57	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎})
59	51, 58	syl6bb 276	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ TosetRel → (𝑚 ∈ (fi‘𝐴) ↔ ∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}))
60	45, 5	syl6eq 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ TosetRel → (fi‘𝐵) = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}))
61	60	eleq2d 2836	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ TosetRel → (𝑛 ∈ (fi‘𝐵) ↔ 𝑛 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})))
62		vex 3354	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
63		breq1 4790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
64	63	notbid 307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑏 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑏𝑅𝑦))
65	64	rabbidv 3339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑏 → {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦})
66	65	cbvmptv 4885	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) = (𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦})
67	66	elrnmpt 5509	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ V → (𝑛 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}))
68	62, 67	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦})
69	61, 68	syl6bb 276	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ TosetRel → (𝑛 ∈ (fi‘𝐵) ↔ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}))
70	59, 69	anbi12d 616	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ TosetRel → ((𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵)) ↔ (∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦})))
71		reeanv 3255	. . . . . . . . . . . . 13 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) ↔ (∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}))
72		ineq12 3960	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → (𝑚 ∩ 𝑛) = ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}))
73		inrab 4047	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}
74	72, 73	syl6eq 2821	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
75	74	reximi 3159	. . . . . . . . . . . . . 14 ⊢ (∃𝑏 ∈ 𝑋 (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
76	75	reximi 3159	. . . . . . . . . . . . 13 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
77	71, 76	sylbir 225	. . . . . . . . . . . 12 ⊢ ((∃𝑎 ∈ 𝑋 𝑚 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∧ ∃𝑏 ∈ 𝑋 𝑛 = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
78	70, 77	syl6bi 243	. . . . . . . . . . 11 ⊢ (𝑅 ∈ TosetRel → ((𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}))
79	78	imp 393	. . . . . . . . . 10 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵))) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
80	52	inex1 4934	. . . . . . . . . . 11 ⊢ (𝑚 ∩ 𝑛) ∈ V
81		eqid 2771	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) = (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
82	81	elrnmpt2g 6923	. . . . . . . . . . 11 ⊢ ((𝑚 ∩ 𝑛) ∈ V → ((𝑚 ∩ 𝑛) ∈ ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}))
83	80, 82	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑚 ∩ 𝑛) ∈ ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑚 ∩ 𝑛) = {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
84	79, 83	sylibr 224	. . . . . . . . 9 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵))) → (𝑚 ∩ 𝑛) ∈ ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}))
85		ordtval.4	. . . . . . . . 9 ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})
86	84, 85	syl6eleqr 2861	. . . . . . . 8 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵))) → (𝑚 ∩ 𝑛) ∈ 𝐶)
87	49, 86	sseldi 3750	. . . . . . 7 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵))) → (𝑚 ∩ 𝑛) ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶))
88		eleq1 2838	. . . . . . 7 ⊢ (𝑧 = (𝑚 ∩ 𝑛) → (𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶) ↔ (𝑚 ∩ 𝑛) ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
89	87, 88	syl5ibrcom 237	. . . . . 6 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑚 ∈ (fi‘𝐴) ∧ 𝑛 ∈ (fi‘𝐵))) → (𝑧 = (𝑚 ∩ 𝑛) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
90	89	rexlimdvva 3186	. . . . 5 ⊢ (𝑅 ∈ TosetRel → (∃𝑚 ∈ (fi‘𝐴)∃𝑛 ∈ (fi‘𝐵)𝑧 = (𝑚 ∩ 𝑛) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
91	25, 48, 90	3jaod 1540	. . . 4 ⊢ (𝑅 ∈ TosetRel → ((𝑧 ∈ (fi‘𝐴) ∨ 𝑧 ∈ (fi‘𝐵) ∨ ∃𝑚 ∈ (fi‘𝐴)∃𝑛 ∈ (fi‘𝐵)𝑧 = (𝑚 ∩ 𝑛)) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
92	20, 91	sylbid 230	. . 3 ⊢ (𝑅 ∈ TosetRel → (𝑧 ∈ (fi‘(𝐴 ∪ 𝐵)) → 𝑧 ∈ ((𝐴 ∪ 𝐵) ∪ 𝐶)))
93	92	ssrdv 3758	. 2 ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) ⊆ ((𝐴 ∪ 𝐵) ∪ 𝐶))
94		ssfii 8485	. . . 4 ⊢ ((𝐴 ∪ 𝐵) ∈ V → (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵)))
95	13, 94	syl 17	. . 3 ⊢ (𝑅 ∈ TosetRel → (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵)))
96	95	adantr 466	. . . . . . . . . 10 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵)))
97		simprl 754	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋)
98		eqidd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎})
99	55	eqeq2d 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥} ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}))
100	99	rspcev 3460	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ 𝑋 ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎}) → ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})
101	97, 98, 100	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})
102	8	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑋 ∈ V)
103		rabexg 4946	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ V → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V)
104		eqid 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})
105	104	elrnmpt 5509	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}))
106	102, 103, 105	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}))
107	101, 106	mpbird 247	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}))
108	107, 4	syl6eleqr 2861	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ 𝐴)
109	1, 108	sseldi 3750	. . . . . . . . . 10 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ (𝐴 ∪ 𝐵))
110	96, 109	sseldd 3753	. . . . . . . . 9 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ (fi‘(𝐴 ∪ 𝐵)))
111		simprr 756	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋)
112		eqidd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦})
113	65	eqeq2d 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦} ↔ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}))
114	113	rspcev 3460	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑋 ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) → ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})
115	111, 112, 114	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})
116		rabexg 4946	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ V → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ V)
117		eqid 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})
118	117	elrnmpt 5509	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ V → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}))
119	102, 116, 118	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ↔ ∃𝑥 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} = {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}))
120	115, 119	mpbird 247	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}))
121	120, 5	syl6eleqr 2861	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ 𝐵)
122	16, 121	sseldi 3750	. . . . . . . . . 10 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ (𝐴 ∪ 𝐵))
123	96, 122	sseldd 3753	. . . . . . . . 9 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ (fi‘(𝐴 ∪ 𝐵)))
124		fiin 8488	. . . . . . . . 9 ⊢ (({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∈ (fi‘(𝐴 ∪ 𝐵)) ∧ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦} ∈ (fi‘(𝐴 ∪ 𝐵))) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) ∈ (fi‘(𝐴 ∪ 𝐵)))
125	110, 123, 124	syl2anc 573	. . . . . . . 8 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ({𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑎} ∩ {𝑦 ∈ 𝑋 ∣ ¬ 𝑏𝑅𝑦}) ∈ (fi‘(𝐴 ∪ 𝐵)))
126	73, 125	syl5eqelr 2855	. . . . . . 7 ⊢ ((𝑅 ∈ TosetRel ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)} ∈ (fi‘(𝐴 ∪ 𝐵)))
127	126	ralrimivva 3120	. . . . . 6 ⊢ (𝑅 ∈ TosetRel → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)} ∈ (fi‘(𝐴 ∪ 𝐵)))
128	81	fmpt2 7391	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)} ∈ (fi‘(𝐴 ∪ 𝐵)) ↔ (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}):(𝑋 × 𝑋)⟶(fi‘(𝐴 ∪ 𝐵)))
129	127, 128	sylib 208	. . . . 5 ⊢ (𝑅 ∈ TosetRel → (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}):(𝑋 × 𝑋)⟶(fi‘(𝐴 ∪ 𝐵)))
130	129	frnd 6191	. . . 4 ⊢ (𝑅 ∈ TosetRel → ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ⊆ (fi‘(𝐴 ∪ 𝐵)))
131	85, 130	syl5eqss 3798	. . 3 ⊢ (𝑅 ∈ TosetRel → 𝐶 ⊆ (fi‘(𝐴 ∪ 𝐵)))
132	95, 131	unssd 3940	. 2 ⊢ (𝑅 ∈ TosetRel → ((𝐴 ∪ 𝐵) ∪ 𝐶) ⊆ (fi‘(𝐴 ∪ 𝐵)))
133	93, 132	eqssd 3769	1 ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∨ w3o 1070   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062  {crab 3065  Vcvv 3351   ∪ cun 3721   ∩ cin 3722   ⊆ wss 3723  {csn 4317  ∪ cuni 4575   class class class wbr 4787   ↦ cmpt 4864   × cxp 5248  ^◡ccnv 5249  dom cdm 5250  ran crn 5251  ⟶wf 6026  ‘cfv 6030   ↦ cmpt2 6798  ficfi 8476  PosetRelcps 17406   TosetRel ctsr 17407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-om 7217  df-1st 7319  df-2nd 7320  df-wrecs 7563  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7900  df-en 8114  df-fin 8117  df-fi 8477  df-ps 17408  df-tsr 17409

This theorem is referenced by:  ordtbas  21217  leordtval  21238