MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtrest Structured version   Visualization version   GIF version

Theorem ordtrest 20916
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.
StepHypRef Expression
1 inex1g 4761 . . . 4 (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
21adantr 481 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
3 eqid 2621 . . . 4 dom (𝑅 ∩ (𝐴 × 𝐴)) = dom (𝑅 ∩ (𝐴 × 𝐴))
4 eqid 2621 . . . 4 ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
5 eqid 2621 . . . 4 ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
63, 4, 5ordtval 20903 . . 3 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))))
72, 6syl 17 . 2 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))))
8 ordttop 20914 . . . 4 (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Top)
9 resttop 20874 . . . 4 (((ordTop‘𝑅) ∈ Top ∧ 𝐴𝑉) → ((ordTop‘𝑅) ↾t 𝐴) ∈ Top)
108, 9sylan 488 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ((ordTop‘𝑅) ↾t 𝐴) ∈ Top)
11 eqid 2621 . . . . . . . 8 dom 𝑅 = dom 𝑅
1211psssdm2 17136 . . . . . . 7 (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅𝐴))
1312adantr 481 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅𝐴))
148adantr 481 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (ordTop‘𝑅) ∈ Top)
15 simpr 477 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → 𝐴𝑉)
1611ordttopon 20907 . . . . . . . . 9 (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ (TopOn‘dom 𝑅))
1716adantr 481 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (ordTop‘𝑅) ∈ (TopOn‘dom 𝑅))
18 toponmax 20643 . . . . . . . 8 ((ordTop‘𝑅) ∈ (TopOn‘dom 𝑅) → dom 𝑅 ∈ (ordTop‘𝑅))
1917, 18syl 17 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → dom 𝑅 ∈ (ordTop‘𝑅))
20 elrestr 16010 . . . . . . 7 (((ordTop‘𝑅) ∈ Top ∧ 𝐴𝑉 ∧ dom 𝑅 ∈ (ordTop‘𝑅)) → (dom 𝑅𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
2114, 15, 19, 20syl3anc 1323 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (dom 𝑅𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
2213, 21eqeltrd 2698 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → dom (𝑅 ∩ (𝐴 × 𝐴)) ∈ ((ordTop‘𝑅) ↾t 𝐴))
2322snssd 4309 . . . 4 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → {dom (𝑅 ∩ (𝐴 × 𝐴))} ⊆ ((ordTop‘𝑅) ↾t 𝐴))
24 rabeq 3179 . . . . . . . . 9 (dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅𝐴) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
2513, 24syl 17 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
2613, 25mpteq12dv 4693 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}))
2726rneqd 5313 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}))
28 inrab2 3876 . . . . . . . . . 10 ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦𝑅𝑥}
29 inss2 3812 . . . . . . . . . . . . . 14 (dom 𝑅𝐴) ⊆ 𝐴
30 simpr 477 . . . . . . . . . . . . . 14 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → 𝑦 ∈ (dom 𝑅𝐴))
3129, 30sseldi 3581 . . . . . . . . . . . . 13 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → 𝑦𝐴)
32 simpr 477 . . . . . . . . . . . . . . 15 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → 𝑥 ∈ (dom 𝑅𝐴))
3329, 32sseldi 3581 . . . . . . . . . . . . . 14 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → 𝑥𝐴)
3433adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → 𝑥𝐴)
35 brinxp 5142 . . . . . . . . . . . . 13 ((𝑦𝐴𝑥𝐴) → (𝑦𝑅𝑥𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
3631, 34, 35syl2anc 692 . . . . . . . . . . . 12 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → (𝑦𝑅𝑥𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
3736notbid 308 . . . . . . . . . . 11 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))
3837rabbidva 3176 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦𝑅𝑥} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
3928, 38syl5eq 2667 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
4014adantr 481 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → (ordTop‘𝑅) ∈ Top)
4115adantr 481 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → 𝐴𝑉)
42 simpl 473 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → 𝑅 ∈ PosetRel)
43 inss1 3811 . . . . . . . . . . . 12 (dom 𝑅𝐴) ⊆ dom 𝑅
4443sseli 3579 . . . . . . . . . . 11 (𝑥 ∈ (dom 𝑅𝐴) → 𝑥 ∈ dom 𝑅)
4511ordtopn1 20908 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅))
4642, 44, 45syl2an 494 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅))
47 elrestr 16010 . . . . . . . . . 10 (((ordTop‘𝑅) ∈ Top ∧ 𝐴𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∈ (ordTop‘𝑅)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
4840, 41, 46, 47syl3anc 1323 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦𝑅𝑥} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
4939, 48eqeltrrd 2699 . . . . . . . 8 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥} ∈ ((ordTop‘𝑅) ↾t 𝐴))
50 eqid 2621 . . . . . . . 8 (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) = (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥})
5149, 50fmptd 6340 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}):(dom 𝑅𝐴)⟶((ordTop‘𝑅) ↾t 𝐴))
52 frn 6010 . . . . . . 7 ((𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}):(dom 𝑅𝐴)⟶((ordTop‘𝑅) ↾t 𝐴) → ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
5351, 52syl 17 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
5427, 53eqsstrd 3618 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
55 rabeq 3179 . . . . . . . . 9 (dom (𝑅 ∩ (𝐴 × 𝐴)) = (dom 𝑅𝐴) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
5613, 55syl 17 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
5713, 56mpteq12dv 4693 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))
5857rneqd 5313 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))
59 inrab2 3876 . . . . . . . . . 10 ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥𝑅𝑦}
60 brinxp 5142 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
6134, 31, 60syl2anc 692 . . . . . . . . . . . 12 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → (𝑥𝑅𝑦𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
6261notbid 308 . . . . . . . . . . 11 ((((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) ∧ 𝑦 ∈ (dom 𝑅𝐴)) → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦))
6362rabbidva 3176 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥𝑅𝑦} = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
6459, 63syl5eq 2667 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
6511ordtopn2 20909 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅))
6642, 44, 65syl2an 494 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅))
67 elrestr 16010 . . . . . . . . . 10 (((ordTop‘𝑅) ∈ Top ∧ 𝐴𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∈ (ordTop‘𝑅)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
6840, 41, 66, 67syl3anc 1323 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → ({𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥𝑅𝑦} ∩ 𝐴) ∈ ((ordTop‘𝑅) ↾t 𝐴))
6964, 68eqeltrrd 2699 . . . . . . . 8 (((𝑅 ∈ PosetRel ∧ 𝐴𝑉) ∧ 𝑥 ∈ (dom 𝑅𝐴)) → {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦} ∈ ((ordTop‘𝑅) ↾t 𝐴))
70 eqid 2621 . . . . . . . 8 (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) = (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})
7169, 70fmptd 6340 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}):(dom 𝑅𝐴)⟶((ordTop‘𝑅) ↾t 𝐴))
72 frn 6010 . . . . . . 7 ((𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}):(dom 𝑅𝐴)⟶((ordTop‘𝑅) ↾t 𝐴) → ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
7371, 72syl 17 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ (dom 𝑅𝐴) ↦ {𝑦 ∈ (dom 𝑅𝐴) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
7458, 73eqsstrd 3618 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
7554, 74unssd 3767 . . . 4 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦})) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
7623, 75unssd 3767 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → ({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
77 tgfiss 20706 . . 3 ((((ordTop‘𝑅) ↾t 𝐴) ∈ Top ∧ ({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) → (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
7810, 76, 77syl2anc 692 . 2 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (topGen‘(fi‘({dom (𝑅 ∩ (𝐴 × 𝐴))} ∪ (ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥}) ∪ ran (𝑥 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦}))))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
797, 78eqsstrd 3618 1 ((𝑅 ∈ PosetRel ∧ 𝐴𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  {crab 2911  Vcvv 3186  cun 3553  cin 3554  wss 3555  {csn 4148   class class class wbr 4613  cmpt 4673   × cxp 5072  dom cdm 5074  ran crn 5075  wf 5843  cfv 5847  (class class class)co 6604  ficfi 8260  t crest 16002  topGenctg 16019  ordTopcordt 16080  PosetRelcps 17119  Topctop 20617  TopOnctopon 20618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-ordt 16082  df-ps 17121  df-top 20621  df-bases 20622  df-topon 20623
This theorem is referenced by:  ordtrest2  20918
  Copyright terms: Public domain W3C validator