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

Theorem ordtrest 23134
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 5323 . . . 4 (𝑅 ∈ PosetRel β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V)
21adantr 479 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V)
3 eqid 2728 . . . 4 dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = dom (𝑅 ∩ (𝐴 Γ— 𝐴))
4 eqid 2728 . . . 4 ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) = ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯})
5 eqid 2728 . . . 4 ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}) = ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦})
63, 4, 5ordtval 23121 . . 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 23132 . . . 4 (𝑅 ∈ PosetRel β†’ (ordTopβ€˜π‘…) ∈ Top)
9 resttop 23092 . . . 4 (((ordTopβ€˜π‘…) ∈ Top ∧ 𝐴 ∈ 𝑉) β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) ∈ Top)
108, 9sylan 578 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) ∈ Top)
11 eqid 2728 . . . . . . . 8 dom 𝑅 = dom 𝑅
1211psssdm2 18582 . . . . . . 7 (𝑅 ∈ PosetRel β†’ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = (dom 𝑅 ∩ 𝐴))
1312adantr 479 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = (dom 𝑅 ∩ 𝐴))
148adantr 479 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (ordTopβ€˜π‘…) ∈ Top)
15 simpr 483 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ 𝐴 ∈ 𝑉)
1611ordttopon 23125 . . . . . . . . 9 (𝑅 ∈ PosetRel β†’ (ordTopβ€˜π‘…) ∈ (TopOnβ€˜dom 𝑅))
1716adantr 479 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (ordTopβ€˜π‘…) ∈ (TopOnβ€˜dom 𝑅))
18 toponmax 22856 . . . . . . . 8 ((ordTopβ€˜π‘…) ∈ (TopOnβ€˜dom 𝑅) β†’ dom 𝑅 ∈ (ordTopβ€˜π‘…))
1917, 18syl 17 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ dom 𝑅 ∈ (ordTopβ€˜π‘…))
20 elrestr 17419 . . . . . . 7 (((ordTopβ€˜π‘…) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ dom 𝑅 ∈ (ordTopβ€˜π‘…)) β†’ (dom 𝑅 ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
2114, 15, 19, 20syl3anc 1368 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (dom 𝑅 ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
2213, 21eqeltrd 2829 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
2322snssd 4817 . . . 4 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ {dom (𝑅 ∩ (𝐴 Γ— 𝐴))} βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
2413rabeqdv 3446 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯})
2513, 24mpteq12dv 5243 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) = (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}))
2625rneqd 5944 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) = ran (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}))
27 inrab2 4310 . . . . . . . . . 10 ({𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦𝑅π‘₯}
28 simpr 483 . . . . . . . . . . . . . 14 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ 𝑦 ∈ (dom 𝑅 ∩ 𝐴))
2928elin2d 4201 . . . . . . . . . . . . 13 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ 𝑦 ∈ 𝐴)
30 simpr 483 . . . . . . . . . . . . . . 15 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ π‘₯ ∈ (dom 𝑅 ∩ 𝐴))
3130elin2d 4201 . . . . . . . . . . . . . 14 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ π‘₯ ∈ 𝐴)
3231adantr 479 . . . . . . . . . . . . 13 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ π‘₯ ∈ 𝐴)
33 brinxp 5760 . . . . . . . . . . . . 13 ((𝑦 ∈ 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (𝑦𝑅π‘₯ ↔ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯))
3429, 32, 33syl2anc 582 . . . . . . . . . . . 12 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ (𝑦𝑅π‘₯ ↔ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯))
3534notbid 317 . . . . . . . . . . 11 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ (Β¬ 𝑦𝑅π‘₯ ↔ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯))
3635rabbidva 3437 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦𝑅π‘₯} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯})
3727, 36eqtrid 2780 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯})
3814adantr 479 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ (ordTopβ€˜π‘…) ∈ Top)
3915adantr 479 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ 𝐴 ∈ 𝑉)
40 simpl 481 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ 𝑅 ∈ PosetRel)
41 elinel1 4197 . . . . . . . . . . 11 (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) β†’ π‘₯ ∈ dom 𝑅)
4211ordtopn1 23126 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ π‘₯ ∈ dom 𝑅) β†’ {𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
4340, 41, 42syl2an 594 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…))
44 elrestr 17419 . . . . . . . . . 10 (((ordTopβ€˜π‘…) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∈ (ordTopβ€˜π‘…)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
4538, 39, 43, 44syl3anc 1368 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ 𝑦𝑅π‘₯} ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
4637, 45eqeltrrd 2830 . . . . . . . 8 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯} ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
4746fmpttd 7130 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}):(dom 𝑅 ∩ 𝐴)⟢((ordTopβ€˜π‘…) β†Ύt 𝐴))
4847frnd 6735 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
4926, 48eqsstrd 4020 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
5013rabeqdv 3446 . . . . . . . 8 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦})
5113, 50mpteq12dv 5243 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}) = (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))
5251rneqd 5944 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}) = ran (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))
53 inrab2 4310 . . . . . . . . . 10 ({𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯𝑅𝑦}
54 brinxp 5760 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯𝑅𝑦 ↔ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦))
5532, 29, 54syl2anc 582 . . . . . . . . . . . 12 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ (π‘₯𝑅𝑦 ↔ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦))
5655notbid 317 . . . . . . . . . . 11 ((((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) ∧ 𝑦 ∈ (dom 𝑅 ∩ 𝐴)) β†’ (Β¬ π‘₯𝑅𝑦 ↔ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦))
5756rabbidva 3437 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯𝑅𝑦} = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦})
5853, 57eqtrid 2780 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝐴) = {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦})
5911ordtopn2 23127 . . . . . . . . . . 11 ((𝑅 ∈ PosetRel ∧ π‘₯ ∈ dom 𝑅) β†’ {𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…))
6040, 41, 59syl2an 594 . . . . . . . . . 10 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…))
61 elrestr 17419 . . . . . . . . . 10 (((ordTopβ€˜π‘…) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ {𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∈ (ordTopβ€˜π‘…)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6238, 39, 60, 61syl3anc 1368 . . . . . . . . 9 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ ({𝑦 ∈ dom 𝑅 ∣ Β¬ π‘₯𝑅𝑦} ∩ 𝐴) ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6358, 62eqeltrrd 2830 . . . . . . . 8 (((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) ∧ π‘₯ ∈ (dom 𝑅 ∩ 𝐴)) β†’ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦} ∈ ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6463fmpttd 7130 . . . . . . 7 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}):(dom 𝑅 ∩ 𝐴)⟢((ordTopβ€˜π‘…) β†Ύt 𝐴))
6564frnd 6735 . . . . . 6 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ (dom 𝑅 ∩ 𝐴) ↦ {𝑦 ∈ (dom 𝑅 ∩ 𝐴) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6652, 65eqsstrd 4020 . . . . 5 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6749, 66unssd 4188 . . . 4 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βˆͺ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦})) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
6823, 67unssd 4188 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ ({dom (𝑅 ∩ (𝐴 Γ— 𝐴))} βˆͺ (ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βˆͺ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
69 tgfiss 22922 . . 3 ((((ordTopβ€˜π‘…) β†Ύt 𝐴) ∈ Top ∧ ({dom (𝑅 ∩ (𝐴 Γ— 𝐴))} βˆͺ (ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βˆͺ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴)) β†’ (topGenβ€˜(fiβ€˜({dom (𝑅 ∩ (𝐴 Γ— 𝐴))} βˆͺ (ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βˆͺ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
7010, 68, 69syl2anc 582 . 2 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (topGenβ€˜(fiβ€˜({dom (𝑅 ∩ (𝐴 Γ— 𝐴))} βˆͺ (ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ 𝑦(𝑅 ∩ (𝐴 Γ— 𝐴))π‘₯}) βˆͺ ran (π‘₯ ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ↦ {𝑦 ∈ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) ∣ Β¬ π‘₯(𝑅 ∩ (𝐴 Γ— 𝐴))𝑦}))))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
717, 70eqsstrd 4020 1 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {crab 3430  Vcvv 3473   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  {csn 4632   class class class wbr 5152   ↦ cmpt 5235   Γ— cxp 5680  dom cdm 5682  ran crn 5683  β€˜cfv 6553  (class class class)co 7426  ficfi 9443   β†Ύt crest 17411  topGenctg 17428  ordTopcordt 17490  PosetRelcps 18565  Topctop 22823  TopOnctopon 22840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-1st 8001  df-2nd 8002  df-1o 8495  df-er 8733  df-en 8973  df-fin 8976  df-fi 9444  df-rest 17413  df-topgen 17434  df-ordt 17492  df-ps 18567  df-top 22824  df-topon 22841  df-bases 22877
This theorem is referenced by:  ordtrest2  23136
  Copyright terms: Public domain W3C validator