MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtrest2 Structured version   Visualization version   GIF version
Theorem ordtrest2 22715
Description: An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like β„š there are interval-closed sets like (Ο€, +∞) ∩ β„š that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
ordtrest2.1 𝑋 = dom 𝑅
ordtrest2.2 (πœ‘ β†’ 𝑅 ∈ TosetRel )
ordtrest2.3 (πœ‘ β†’ 𝐴 βŠ† 𝑋)
ordtrest2.4 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝑋 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)} βŠ† 𝐴)
Assertion
Ref Expression
ordtrest2 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) = ((ordTopβ€˜π‘…) β†Ύt 𝐴))
Distinct variable groups:   π‘₯,𝑦,𝑧,𝐴   πœ‘,π‘₯,𝑦,𝑧   π‘₯,𝑅,𝑦,𝑧   π‘₯,𝑋,𝑦,𝑧
Proof of Theorem ordtrest2
Dummy variables 𝑀 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtrest2.2 . . . 4 (πœ‘ β†’ 𝑅 ∈ TosetRel )
2 tsrps 18542 . . . 4 (𝑅 ∈ TosetRel β†’ 𝑅 ∈ PosetRel)
31, 2syl 17 . . 3 (πœ‘ β†’ 𝑅 ∈ PosetRel)
4 ordtrest2.1 . . . . 5 𝑋 = dom 𝑅
51dmexd 7898 . . . . 5 (πœ‘ β†’ dom 𝑅 ∈ V)
64, 5eqeltrid 2837 . . . 4 (πœ‘ β†’ 𝑋 ∈ V)
7 ordtrest2.3 . . . 4 (πœ‘ β†’ 𝐴 βŠ† 𝑋)
86, 7ssexd 5324 . . 3 (πœ‘ β†’ 𝐴 ∈ V)
9 ordtrest 22713 . . 3 ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ V) β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
103, 8, 9syl2anc 584 . 2 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) βŠ† ((ordTopβ€˜π‘…) β†Ύt 𝐴))
11 eqid 2732 . . . . . . . 8 ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) = ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧})
12 eqid 2732 . . . . . . . 8 ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}) = ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})
134, 11, 12ordtval 22700 . . . . . . 7 (𝑅 ∈ TosetRel β†’ (ordTopβ€˜π‘…) = (topGenβ€˜(fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))))
141, 13syl 17 . . . . . 6 (πœ‘ β†’ (ordTopβ€˜π‘…) = (topGenβ€˜(fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))))
1514oveq1d 7426 . . . . 5 (πœ‘ β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) = ((topGenβ€˜(fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))) β†Ύt 𝐴))
16 fibas 22487 . . . . . 6 (fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) ∈ TopBases
17 tgrest 22670 . . . . . 6 (((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) ∈ TopBases ∧ 𝐴 ∈ V) β†’ (topGenβ€˜((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) β†Ύt 𝐴)) = ((topGenβ€˜(fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))) β†Ύt 𝐴))
1816, 8, 17sylancr 587 . . . . 5 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) β†Ύt 𝐴)) = ((topGenβ€˜(fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))) β†Ύt 𝐴))
1915, 18eqtr4d 2775 . . . 4 (πœ‘ β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) = (topGenβ€˜((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) β†Ύt 𝐴)))
20 firest 17380 . . . . 5 (fiβ€˜(({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴)) = ((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) β†Ύt 𝐴)
2120fveq2i 6894 . . . 4 (topGenβ€˜(fiβ€˜(({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴))) = (topGenβ€˜((fiβ€˜({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))) β†Ύt 𝐴))
2219, 21eqtr4di 2790 . . 3 (πœ‘ β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) = (topGenβ€˜(fiβ€˜(({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴))))
23 inex1g 5319 . . . . . 6 (𝑅 ∈ TosetRel β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V)
241, 23syl 17 . . . . 5 (πœ‘ β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V)
25 ordttop 22711 . . . . 5 ((𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ Top)
2624, 25syl 17 . . . 4 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ Top)
274, 11, 12ordtuni 22701 . . . . . . . . 9 (𝑅 ∈ TosetRel β†’ 𝑋 = βˆͺ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))
281, 27syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑋 = βˆͺ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))))
2928, 6eqeltrrd 2834 . . . . . . 7 (πœ‘ β†’ βˆͺ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ∈ V)
30 uniexb 7753 . . . . . . 7 (({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ∈ V ↔ βˆͺ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ∈ V)
3129, 30sylibr 233 . . . . . 6 (πœ‘ β†’ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ∈ V)
32 restval 17374 . . . . . 6 ((({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ∈ V ∧ 𝐴 ∈ V) β†’ (({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴) = ran (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)))
3331, 8, 32syl2anc 584 . . . . 5 (πœ‘ β†’ (({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴) = ran (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)))
34 sseqin2 4215 . . . . . . . . . . . 12 (𝐴 βŠ† 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
357, 34sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ (𝑋 ∩ 𝐴) = 𝐴)
36 eqid 2732 . . . . . . . . . . . . . . 15 dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = dom (𝑅 ∩ (𝐴 Γ— 𝐴))
3736ordttopon 22704 . . . . . . . . . . . . . 14 ((𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ V β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜dom (𝑅 ∩ (𝐴 Γ— 𝐴))))
3824, 37syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜dom (𝑅 ∩ (𝐴 Γ— 𝐴))))
394psssdm 18537 . . . . . . . . . . . . . . 15 ((𝑅 ∈ PosetRel ∧ 𝐴 βŠ† 𝑋) β†’ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = 𝐴)
403, 7, 39syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ dom (𝑅 ∩ (𝐴 Γ— 𝐴)) = 𝐴)
4140fveq2d 6895 . . . . . . . . . . . . 13 (πœ‘ β†’ (TopOnβ€˜dom (𝑅 ∩ (𝐴 Γ— 𝐴))) = (TopOnβ€˜π΄))
4238, 41eleqtrd 2835 . . . . . . . . . . . 12 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜π΄))
43 toponmax 22435 . . . . . . . . . . . 12 ((ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜π΄) β†’ 𝐴 ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
4442, 43syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
4535, 44eqeltrd 2833 . . . . . . . . . 10 (πœ‘ β†’ (𝑋 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
46 elsni 4645 . . . . . . . . . . . 12 (𝑣 ∈ {𝑋} β†’ 𝑣 = 𝑋)
4746ineq1d 4211 . . . . . . . . . . 11 (𝑣 ∈ {𝑋} β†’ (𝑣 ∩ 𝐴) = (𝑋 ∩ 𝐴))
4847eleq1d 2818 . . . . . . . . . 10 (𝑣 ∈ {𝑋} β†’ ((𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ (𝑋 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴)))))
4945, 48syl5ibrcom 246 . . . . . . . . 9 (πœ‘ β†’ (𝑣 ∈ {𝑋} β†’ (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴)))))
5049ralrimiv 3145 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘£ ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
51 ordtrest2.4 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝑋 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)} βŠ† 𝐴)
524, 1, 7, 51ordtrest2lem 22714 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
53 df-rn 5687 . . . . . . . . . . 11 ran 𝑅 = dom ◑𝑅
54 cnvtsr 18543 . . . . . . . . . . . 12 (𝑅 ∈ TosetRel β†’ ◑𝑅 ∈ TosetRel )
551, 54syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ◑𝑅 ∈ TosetRel )
564psrn 18530 . . . . . . . . . . . . 13 (𝑅 ∈ PosetRel β†’ 𝑋 = ran 𝑅)
573, 56syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 = ran 𝑅)
587, 57sseqtrd 4022 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† ran 𝑅)
5957adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ 𝑋 = ran 𝑅)
6059rabeqdv 3447 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝑋 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)})
61 vex 3478 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
62 vex 3478 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6361, 62brcnv 5882 . . . . . . . . . . . . . . . 16 (𝑦◑𝑅𝑧 ↔ 𝑧𝑅𝑦)
64 vex 3478 . . . . . . . . . . . . . . . . 17 π‘₯ ∈ V
6562, 64brcnv 5882 . . . . . . . . . . . . . . . 16 (𝑧◑𝑅π‘₯ ↔ π‘₯𝑅𝑧)
6663, 65anbi12ci 628 . . . . . . . . . . . . . . 15 ((𝑦◑𝑅𝑧 ∧ 𝑧◑𝑅π‘₯) ↔ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦))
6766rabbii 3438 . . . . . . . . . . . . . 14 {𝑧 ∈ ran 𝑅 ∣ (𝑦◑𝑅𝑧 ∧ 𝑧◑𝑅π‘₯)} = {𝑧 ∈ ran 𝑅 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)}
6860, 67eqtr4di 2790 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝑋 ∣ (π‘₯𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑦◑𝑅𝑧 ∧ 𝑧◑𝑅π‘₯)})
6968, 51eqsstrrd 4021 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ ran 𝑅 ∣ (𝑦◑𝑅𝑧 ∧ 𝑧◑𝑅π‘₯)} βŠ† 𝐴)
7069ancom2s 648 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐴 ∧ π‘₯ ∈ 𝐴)) β†’ {𝑧 ∈ ran 𝑅 ∣ (𝑦◑𝑅𝑧 ∧ 𝑧◑𝑅π‘₯)} βŠ† 𝐴)
7153, 55, 58, 70ordtrest2lem 22714 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑀 ∈ ran 𝑅 ∣ Β¬ 𝑀◑𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(◑𝑅 ∩ (𝐴 Γ— 𝐴))))
72 vex 3478 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
7372, 62brcnv 5882 . . . . . . . . . . . . . . . . 17 (𝑀◑𝑅𝑧 ↔ 𝑧𝑅𝑀)
7473bicomi 223 . . . . . . . . . . . . . . . 16 (𝑧𝑅𝑀 ↔ 𝑀◑𝑅𝑧)
7574a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑧𝑅𝑀 ↔ 𝑀◑𝑅𝑧))
7675notbid 317 . . . . . . . . . . . . . 14 (πœ‘ β†’ (Β¬ 𝑧𝑅𝑀 ↔ Β¬ 𝑀◑𝑅𝑧))
7757, 76rabeqbidv 3449 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀} = {𝑀 ∈ ran 𝑅 ∣ Β¬ 𝑀◑𝑅𝑧})
7857, 77mpteq12dv 5239 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}) = (𝑧 ∈ ran 𝑅 ↦ {𝑀 ∈ ran 𝑅 ∣ Β¬ 𝑀◑𝑅𝑧}))
7978rneqd 5937 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}) = ran (𝑧 ∈ ran 𝑅 ↦ {𝑀 ∈ ran 𝑅 ∣ Β¬ 𝑀◑𝑅𝑧}))
80 psss 18535 . . . . . . . . . . . . . . 15 (𝑅 ∈ PosetRel β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ PosetRel)
813, 80syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ PosetRel)
82 ordtcnv 22712 . . . . . . . . . . . . . 14 ((𝑅 ∩ (𝐴 Γ— 𝐴)) ∈ PosetRel β†’ (ordTopβ€˜β—‘(𝑅 ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
8381, 82syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (ordTopβ€˜β—‘(𝑅 ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
84 cnvin 6144 . . . . . . . . . . . . . . 15 β—‘(𝑅 ∩ (𝐴 Γ— 𝐴)) = (◑𝑅 ∩ β—‘(𝐴 Γ— 𝐴))
85 cnvxp 6156 . . . . . . . . . . . . . . . 16 β—‘(𝐴 Γ— 𝐴) = (𝐴 Γ— 𝐴)
8685ineq2i 4209 . . . . . . . . . . . . . . 15 (◑𝑅 ∩ β—‘(𝐴 Γ— 𝐴)) = (◑𝑅 ∩ (𝐴 Γ— 𝐴))
8784, 86eqtri 2760 . . . . . . . . . . . . . 14 β—‘(𝑅 ∩ (𝐴 Γ— 𝐴)) = (◑𝑅 ∩ (𝐴 Γ— 𝐴))
8887fveq2i 6894 . . . . . . . . . . . . 13 (ordTopβ€˜β—‘(𝑅 ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(◑𝑅 ∩ (𝐴 Γ— 𝐴)))
8983, 88eqtr3di 2787 . . . . . . . . . . . 12 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(◑𝑅 ∩ (𝐴 Γ— 𝐴))))
9089eleq2d 2819 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(◑𝑅 ∩ (𝐴 Γ— 𝐴)))))
9179, 90raleqbidv 3342 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘£ ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ βˆ€π‘£ ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑀 ∈ ran 𝑅 ∣ Β¬ 𝑀◑𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(◑𝑅 ∩ (𝐴 Γ— 𝐴)))))
9271, 91mpbird 256 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
93 ralunb 4191 . . . . . . . . 9 (βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ (βˆ€π‘£ ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∧ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴)))))
9452, 92, 93sylanbrc 583 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
95 ralunb 4191 . . . . . . . 8 (βˆ€π‘£ ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ (βˆ€π‘£ ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∧ βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴)))))
9650, 94, 95sylanbrc 583 . . . . . . 7 (πœ‘ β†’ βˆ€π‘£ ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
97 eqid 2732 . . . . . . . 8 (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴))
9897fmpt 7111 . . . . . . 7 (βˆ€π‘£ ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ↔ (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))⟢(ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
9996, 98sylib 217 . . . . . 6 (πœ‘ β†’ (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀})))⟢(ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
10099frnd 6725 . . . . 5 (πœ‘ β†’ ran (𝑣 ∈ ({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) ↦ (𝑣 ∩ 𝐴)) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
10133, 100eqsstrd 4020 . . . 4 (πœ‘ β†’ (({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
102 tgfiss 22501 . . . 4 (((ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) ∈ Top ∧ (({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴)))) β†’ (topGenβ€˜(fiβ€˜(({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴))) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
10326, 101, 102syl2anc 584 . . 3 (πœ‘ β†’ (topGenβ€˜(fiβ€˜(({𝑋} βˆͺ (ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑀𝑅𝑧}) βˆͺ ran (𝑧 ∈ 𝑋 ↦ {𝑀 ∈ 𝑋 ∣ Β¬ 𝑧𝑅𝑀}))) β†Ύt 𝐴))) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
10422, 103eqsstrd 4020 . 2 (πœ‘ β†’ ((ordTopβ€˜π‘…) β†Ύt 𝐴) βŠ† (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))))
10510, 104eqssd 3999 1 (πœ‘ β†’ (ordTopβ€˜(𝑅 ∩ (𝐴 Γ— 𝐴))) = ((ordTopβ€˜π‘…) β†Ύt 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  {csn 4628  βˆͺ cuni 4908   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  ficfi 9407   β†Ύt crest 17368  topGenctg 17385  ordTopcordt 17447  PosetRelcps 18519   TosetRel ctsr 18520  Topctop 22402  TopOnctopon 22419  TopBasesctb 22455
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-rest 17370  df-topgen 17391  df-ordt 17449  df-ps 18521  df-tsr 18522  df-top 22403  df-topon 22420  df-bases 22456
This theorem is referenced by:  ordtrestixx  22733  cnvordtrestixx  32962
  Copyright terms: Public domain W3C validator