Theorem ordtrest 22553

Description: The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.)

Assertion

Ref	Expression
ordtrest	⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))

Proof of Theorem ordtrest

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inex1g 5276	. . . 4 ⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
2	1	adantr 481	. . 3 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
3		eqid 2736	. . . 4 ⊢ dom (𝑅 ∩ (𝐴 × 𝐴)) = dom (𝑅 ∩ (𝐴 × 𝐴))
4		eqid 2736	. . . 4 ⊢ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
5		eqid 2736	. . . 4 ⊢ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
6	3, 4, 5	ordtval 22540	. . 3 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))))
7	2, 6	syl 17	. 2 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))))
8		ordttop 22551	. . . 4 ⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Top)
9		resttop 22511	. . . 4 ⊢ (((ordTop‘𝑅) ∈ Top ∧ 𝐴 ∈ 𝑉) → ((ordTop‘𝑅) ↾t 𝐴) ∈ Top)
10	8, 9	sylan 580	. . 3 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ((ordTop‘𝑅) ↾t 𝐴) ∈ Top)
11		eqid 2736	. . . . . . . 8 ⊢ dom 𝑅 = dom 𝑅
12	11	psssdm2 18470	. . . . . . 7 ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅 ∩ 𝐴))
13	12	adantr 481	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅 ∩ 𝐴))
14	8	adantr 481	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘𝑅) ∈ Top)
15		simpr 485	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉)
16	11	ordttopon 22544	. . . . . . . . 9 ⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ (TopOn‘dom 𝑅))
17	16	adantr 481	. . . . . . . 8 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘𝑅) ∈ (TopOn‘dom 𝑅))
18		toponmax 22275	. . . . . . . 8 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘dom 𝑅) → dom 𝑅 ∈ (ordTop‘𝑅))
19	17, 18	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → dom 𝑅 ∈ (ordTop‘𝑅))
20		elrestr 17310	. . . . . . 7 ⊢ (((ordTop‘𝑅) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ dom 𝑅 ∈ (ordTop‘𝑅)) → (dom 𝑅 ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
21	14, 15, 19, 20	syl3anc 1371	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (dom 𝑅 ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
22	13, 21	eqeltrd 2838	. . . . 5 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → dom (𝑅 ∩ (𝐴 × 𝐴)) ∈ ((ordTop‘𝑅) ↾t 𝐴))
23	22	snssd 4769	. . . 4 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → {dom (𝑅 ∩ (𝐴 × 𝐴))} ⊆ ((ordTop‘𝑅) ↾t 𝐴))
24	13	rabeqdv 3422	. . . . . . . 8 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
25	13, 24	mpteq12dv 5196	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}))
26	25	rneqd 5893	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}))
27		inrab2 4267	. . . . . . . . . 10 ⊢ ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦𝑅𝑥}
28		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → 𝑦 ∈ (dom 𝑅 ∩ 𝐴))
29	28	elin2d 4159	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → 𝑦 ∈ 𝐴)
30		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → 𝑥 ∈ (dom 𝑅 ∩ 𝐴))
31	30	elin2d 4159	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → 𝑥 ∈ 𝐴)
32	31	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → 𝑥 ∈ 𝐴)
33		brinxp 5710	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
34	29, 32, 33	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
35	34	notbid 317	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
36	35	rabbidva 3414	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
37	27, 36	eqtrid 2788	. . . . . . . . 9 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
38	14	adantr 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → (ordTop‘𝑅) ∈ Top)
39	15	adantr 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → 𝐴 ∈ 𝑉)
40		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ PosetRel)
41		elinel1 4155	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (dom 𝑅 ∩ 𝐴) → 𝑥 ∈ dom 𝑅)
42	11	ordtopn1 22545	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅))
43	40, 41, 42	syl2an 596	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅))
44		elrestr 17310	. . . . . . . . . 10 ⊢ (((ordTop‘𝑅) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
45	38, 39, 43, 44	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
46	37, 45	eqeltrrd 2839	. . . . . . . 8 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥} ∈ ((ordTop‘𝑅) ↾t 𝐴))
47	46	fmpttd 7063	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}):(dom 𝑅 ∩ 𝐴)⟶((ordTop‘𝑅) ↾t 𝐴))
48	47	frnd 6676	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
49	26, 48	eqsstrd 3982	. . . . 5 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
50	13	rabeqdv 3422	. . . . . . . 8 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
51	13, 50	mpteq12dv 5196	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))
52	51	rneqd 5893	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))
53		inrab2 4267	. . . . . . . . . 10 ⊢ ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥𝑅𝑦}
54		brinxp 5710	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
55	32, 29, 54	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → (𝑥𝑅𝑦 ↔ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
56	55	notbid 317	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
57	56	rabbidva 3414	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥𝑅𝑦} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
58	53, 57	eqtrid 2788	. . . . . . . . 9 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
59	11	ordtopn2 22546	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅))
60	40, 41, 59	syl2an 596	. . . . . . . . . 10 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅))
61		elrestr 17310	. . . . . . . . . 10 ⊢ (((ordTop‘𝑅) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
62	38, 39, 60, 61	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
63	58, 62	eqeltrrd 2839	. . . . . . . 8 ⊢ (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ (dom 𝑅 ∩ 𝐴)) → {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦} ∈ ((ordTop‘𝑅) ↾t 𝐴))
64	63	fmpttd 7063	. . . . . . 7 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}):(dom 𝑅 ∩ 𝐴)⟶((ordTop‘𝑅) ↾t 𝐴))
65	64	frnd 6676	. . . . . 6 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
66	52, 65	eqsstrd 3982	. . . . 5 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
67	49, 66	unssd 4146	. . . 4 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
68	23, 67	unssd 4146	. . 3 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → ({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
69		tgfiss 22341	. . 3 ⊢ ((((ordTop‘𝑅) ↾t 𝐴) ∈ Top ∧ ({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) → (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
70	10, 68, 69	syl2anc 584	. 2 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
71	7, 70	eqsstrd 3982	1 ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3407  Vcvv 3445   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  {csn 4586   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634  ‘cfv 6496  (class class class)co 7357  ficfi 9346   ↾_t crest 17302  topGenctg 17319  ordTopcordt 17381  PosetRelcps 18453  Topctop 22242  TopOnctopon 22259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-en 8884  df-fin 8887  df-fi 9347  df-rest 17304  df-topgen 17325  df-ordt 17383  df-ps 18455  df-top 22243  df-topon 22260  df-bases 22296

This theorem is referenced by:  ordtrest2  22555