Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordtrest2NEW Structured version   Visualization version   GIF version

Theorem ordtrest2NEW 32544
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.) (Revised by Thierry Arnoux, 11-Sep-2018.)
Hypotheses
Ref Expression
ordtNEW.b 𝐡 = (Baseβ€˜πΎ)
ordtNEW.l ≀ = ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
ordtrest2NEW.2 (πœ‘ β†’ 𝐾 ∈ Toset)
ordtrest2NEW.3 (πœ‘ β†’ 𝐴 βŠ† 𝐡)
ordtrest2NEW.4 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝐡 ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)} βŠ† 𝐴)
Assertion
Ref Expression
ordtrest2NEW (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) = ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
Distinct variable groups:   π‘₯,𝑦, ≀   π‘₯,𝐡,𝑦   π‘₯,𝐾,𝑦   π‘₯,𝐴,𝑦,𝑧   𝑧, ≀   𝑧,𝐴   𝑧,𝐡   πœ‘,π‘₯,𝑦,𝑧   𝑧,𝐾

Proof of Theorem ordtrest2NEW
Dummy variables 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtrest2NEW.2 . . . 4 (πœ‘ β†’ 𝐾 ∈ Toset)
2 tospos 18316 . . . 4 (𝐾 ∈ Toset β†’ 𝐾 ∈ Poset)
3 posprs 18212 . . . 4 (𝐾 ∈ Poset β†’ 𝐾 ∈ Proset )
41, 2, 33syl 18 . . 3 (πœ‘ β†’ 𝐾 ∈ Proset )
5 ordtrest2NEW.3 . . 3 (πœ‘ β†’ 𝐴 βŠ† 𝐡)
6 ordtNEW.b . . . 4 𝐡 = (Baseβ€˜πΎ)
7 ordtNEW.l . . . 4 ≀ = ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
86, 7ordtrestNEW 32542 . . 3 ((𝐾 ∈ Proset ∧ 𝐴 βŠ† 𝐡) β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) βŠ† ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
94, 5, 8syl2anc 585 . 2 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) βŠ† ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
10 eqid 2737 . . . . . . . 8 ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) = ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧})
11 eqid 2737 . . . . . . . 8 ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}) = ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})
126, 7, 10, 11ordtprsval 32539 . . . . . . 7 (𝐾 ∈ Proset β†’ (ordTopβ€˜ ≀ ) = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))))
134, 12syl 17 . . . . . 6 (πœ‘ β†’ (ordTopβ€˜ ≀ ) = (topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))))
1413oveq1d 7377 . . . . 5 (πœ‘ β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) = ((topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))) β†Ύt 𝐴))
15 fibas 22343 . . . . . 6 (fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) ∈ TopBases
166fvexi 6861 . . . . . . . 8 𝐡 ∈ V
1716a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ V)
1817, 5ssexd 5286 . . . . . 6 (πœ‘ β†’ 𝐴 ∈ V)
19 tgrest 22526 . . . . . 6 (((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) ∈ TopBases ∧ 𝐴 ∈ V) β†’ (topGenβ€˜((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) β†Ύt 𝐴)) = ((topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))) β†Ύt 𝐴))
2015, 18, 19sylancr 588 . . . . 5 (πœ‘ β†’ (topGenβ€˜((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) β†Ύt 𝐴)) = ((topGenβ€˜(fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))) β†Ύt 𝐴))
2114, 20eqtr4d 2780 . . . 4 (πœ‘ β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) = (topGenβ€˜((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) β†Ύt 𝐴)))
22 firest 17321 . . . . 5 (fiβ€˜(({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴)) = ((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) β†Ύt 𝐴)
2322fveq2i 6850 . . . 4 (topGenβ€˜(fiβ€˜(({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴))) = (topGenβ€˜((fiβ€˜({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))) β†Ύt 𝐴))
2421, 23eqtr4di 2795 . . 3 (πœ‘ β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) = (topGenβ€˜(fiβ€˜(({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴))))
25 fvex 6860 . . . . . . . 8 (leβ€˜πΎ) ∈ V
2625inex1 5279 . . . . . . 7 ((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) ∈ V
277, 26eqeltri 2834 . . . . . 6 ≀ ∈ V
2827inex1 5279 . . . . 5 ( ≀ ∩ (𝐴 Γ— 𝐴)) ∈ V
29 ordttop 22567 . . . . 5 (( ≀ ∩ (𝐴 Γ— 𝐴)) ∈ V β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ Top)
3028, 29mp1i 13 . . . 4 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ Top)
316, 7, 10, 11ordtprsuni 32540 . . . . . . . . 9 (𝐾 ∈ Proset β†’ 𝐡 = βˆͺ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))
324, 31syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐡 = βˆͺ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))))
3332, 17eqeltrrd 2839 . . . . . . 7 (πœ‘ β†’ βˆͺ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ∈ V)
34 uniexb 7703 . . . . . . 7 (({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ∈ V ↔ βˆͺ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ∈ V)
3533, 34sylibr 233 . . . . . 6 (πœ‘ β†’ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ∈ V)
36 restval 17315 . . . . . 6 ((({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ∈ V ∧ 𝐴 ∈ V) β†’ (({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴) = ran (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)))
3735, 18, 36syl2anc 585 . . . . 5 (πœ‘ β†’ (({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴) = ran (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)))
38 sseqin2 4180 . . . . . . . . . . . 12 (𝐴 βŠ† 𝐡 ↔ (𝐡 ∩ 𝐴) = 𝐴)
395, 38sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 ∩ 𝐴) = 𝐴)
40 eqid 2737 . . . . . . . . . . . . . . 15 dom ( ≀ ∩ (𝐴 Γ— 𝐴)) = dom ( ≀ ∩ (𝐴 Γ— 𝐴))
4140ordttopon 22560 . . . . . . . . . . . . . 14 (( ≀ ∩ (𝐴 Γ— 𝐴)) ∈ V β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜dom ( ≀ ∩ (𝐴 Γ— 𝐴))))
4228, 41mp1i 13 . . . . . . . . . . . . 13 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜dom ( ≀ ∩ (𝐴 Γ— 𝐴))))
436, 7prsssdm 32538 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Proset ∧ 𝐴 βŠ† 𝐡) β†’ dom ( ≀ ∩ (𝐴 Γ— 𝐴)) = 𝐴)
444, 5, 43syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ dom ( ≀ ∩ (𝐴 Γ— 𝐴)) = 𝐴)
4544fveq2d 6851 . . . . . . . . . . . . 13 (πœ‘ β†’ (TopOnβ€˜dom ( ≀ ∩ (𝐴 Γ— 𝐴))) = (TopOnβ€˜π΄))
4642, 45eleqtrd 2840 . . . . . . . . . . . 12 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜π΄))
47 toponmax 22291 . . . . . . . . . . . 12 ((ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ (TopOnβ€˜π΄) β†’ 𝐴 ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
4846, 47syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
4939, 48eqeltrd 2838 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
50 elsni 4608 . . . . . . . . . . . 12 (𝑣 ∈ {𝐡} β†’ 𝑣 = 𝐡)
5150ineq1d 4176 . . . . . . . . . . 11 (𝑣 ∈ {𝐡} β†’ (𝑣 ∩ 𝐴) = (𝐡 ∩ 𝐴))
5251eleq1d 2823 . . . . . . . . . 10 (𝑣 ∈ {𝐡} β†’ ((𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ (𝐡 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴)))))
5349, 52syl5ibrcom 247 . . . . . . . . 9 (πœ‘ β†’ (𝑣 ∈ {𝐡} β†’ (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴)))))
5453ralrimiv 3143 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘£ ∈ {𝐡} (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
55 ordtrest2NEW.4 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝐡 ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)} βŠ† 𝐴)
566, 7, 1, 5, 55ordtrest2NEWlem 32543 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
57 eqid 2737 . . . . . . . . . . . 12 (ODualβ€˜πΎ) = (ODualβ€˜πΎ)
5857, 6odubas 18187 . . . . . . . . . . 11 𝐡 = (Baseβ€˜(ODualβ€˜πΎ))
597cnveqi 5835 . . . . . . . . . . . 12 β—‘ ≀ = β—‘((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
60 cnvin 6102 . . . . . . . . . . . . 13 β—‘((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) = (β—‘(leβ€˜πΎ) ∩ β—‘(𝐡 Γ— 𝐡))
61 cnvxp 6114 . . . . . . . . . . . . . 14 β—‘(𝐡 Γ— 𝐡) = (𝐡 Γ— 𝐡)
6261ineq2i 4174 . . . . . . . . . . . . 13 (β—‘(leβ€˜πΎ) ∩ β—‘(𝐡 Γ— 𝐡)) = (β—‘(leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡))
63 eqid 2737 . . . . . . . . . . . . . . 15 (leβ€˜πΎ) = (leβ€˜πΎ)
6457, 63oduleval 18185 . . . . . . . . . . . . . 14 β—‘(leβ€˜πΎ) = (leβ€˜(ODualβ€˜πΎ))
6564ineq1i 4173 . . . . . . . . . . . . 13 (β—‘(leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) = ((leβ€˜(ODualβ€˜πΎ)) ∩ (𝐡 Γ— 𝐡))
6660, 62, 653eqtri 2769 . . . . . . . . . . . 12 β—‘((leβ€˜πΎ) ∩ (𝐡 Γ— 𝐡)) = ((leβ€˜(ODualβ€˜πΎ)) ∩ (𝐡 Γ— 𝐡))
6759, 66eqtri 2765 . . . . . . . . . . 11 β—‘ ≀ = ((leβ€˜(ODualβ€˜πΎ)) ∩ (𝐡 Γ— 𝐡))
6857odutos 31870 . . . . . . . . . . . 12 (𝐾 ∈ Toset β†’ (ODualβ€˜πΎ) ∈ Toset)
691, 68syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (ODualβ€˜πΎ) ∈ Toset)
70 vex 3452 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
71 vex 3452 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
7270, 71brcnv 5843 . . . . . . . . . . . . . . 15 (𝑦◑ ≀ 𝑧 ↔ 𝑧 ≀ 𝑦)
73 vex 3452 . . . . . . . . . . . . . . . 16 π‘₯ ∈ V
7471, 73brcnv 5843 . . . . . . . . . . . . . . 15 (𝑧◑ ≀ π‘₯ ↔ π‘₯ ≀ 𝑧)
7572, 74anbi12ci 629 . . . . . . . . . . . . . 14 ((𝑦◑ ≀ 𝑧 ∧ 𝑧◑ ≀ π‘₯) ↔ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦))
7675rabbii 3416 . . . . . . . . . . . . 13 {𝑧 ∈ 𝐡 ∣ (𝑦◑ ≀ 𝑧 ∧ 𝑧◑ ≀ π‘₯)} = {𝑧 ∈ 𝐡 ∣ (π‘₯ ≀ 𝑧 ∧ 𝑧 ≀ 𝑦)}
7776, 55eqsstrid 3997 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ {𝑧 ∈ 𝐡 ∣ (𝑦◑ ≀ 𝑧 ∧ 𝑧◑ ≀ π‘₯)} βŠ† 𝐴)
7877ancom2s 649 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐴 ∧ π‘₯ ∈ 𝐴)) β†’ {𝑧 ∈ 𝐡 ∣ (𝑦◑ ≀ 𝑧 ∧ 𝑧◑ ≀ π‘₯)} βŠ† 𝐴)
7958, 67, 69, 5, 78ordtrest2NEWlem 32543 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀◑ ≀ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(β—‘ ≀ ∩ (𝐴 Γ— 𝐴))))
80 vex 3452 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ V
8180, 71brcnv 5843 . . . . . . . . . . . . . . . . 17 (𝑀◑ ≀ 𝑧 ↔ 𝑧 ≀ 𝑀)
8281bicomi 223 . . . . . . . . . . . . . . . 16 (𝑧 ≀ 𝑀 ↔ 𝑀◑ ≀ 𝑧)
8382a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑧 ≀ 𝑀 ↔ 𝑀◑ ≀ 𝑧))
8483notbid 318 . . . . . . . . . . . . . 14 (πœ‘ β†’ (Β¬ 𝑧 ≀ 𝑀 ↔ Β¬ 𝑀◑ ≀ 𝑧))
8584rabbidv 3418 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀} = {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀◑ ≀ 𝑧})
8685mpteq2dv 5212 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}) = (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀◑ ≀ 𝑧}))
8786rneqd 5898 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}) = ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀◑ ≀ 𝑧}))
886ressprs 31865 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Proset ∧ 𝐴 βŠ† 𝐡) β†’ (𝐾 β†Ύs 𝐴) ∈ Proset )
894, 5, 88syl2anc 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐾 β†Ύs 𝐴) ∈ Proset )
90 eqid 2737 . . . . . . . . . . . . . . . 16 (Baseβ€˜(𝐾 β†Ύs 𝐴)) = (Baseβ€˜(𝐾 β†Ύs 𝐴))
91 eqid 2737 . . . . . . . . . . . . . . . 16 ((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴)))) = ((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))
9290, 91ordtcnvNEW 32541 . . . . . . . . . . . . . . 15 ((𝐾 β†Ύs 𝐴) ∈ Proset β†’ (ordTopβ€˜β—‘((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))) = (ordTopβ€˜((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))))
9389, 92syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (ordTopβ€˜β—‘((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))) = (ordTopβ€˜((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))))
946, 7prsss 32537 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Proset ∧ 𝐴 βŠ† 𝐡) β†’ ( ≀ ∩ (𝐴 Γ— 𝐴)) = ((leβ€˜πΎ) ∩ (𝐴 Γ— 𝐴)))
954, 5, 94syl2anc 585 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ( ≀ ∩ (𝐴 Γ— 𝐴)) = ((leβ€˜πΎ) ∩ (𝐴 Γ— 𝐴)))
96 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝐾 β†Ύs 𝐴) = (𝐾 β†Ύs 𝐴)
9796, 63ressle 17268 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ V β†’ (leβ€˜πΎ) = (leβ€˜(𝐾 β†Ύs 𝐴)))
9818, 97syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (leβ€˜πΎ) = (leβ€˜(𝐾 β†Ύs 𝐴)))
9996, 6ressbas2 17127 . . . . . . . . . . . . . . . . . . . 20 (𝐴 βŠ† 𝐡 β†’ 𝐴 = (Baseβ€˜(𝐾 β†Ύs 𝐴)))
1005, 99syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 = (Baseβ€˜(𝐾 β†Ύs 𝐴)))
101100sqxpeqd 5670 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 Γ— 𝐴) = ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))
10298, 101ineq12d 4178 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((leβ€˜πΎ) ∩ (𝐴 Γ— 𝐴)) = ((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴)))))
10395, 102eqtrd 2777 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ( ≀ ∩ (𝐴 Γ— 𝐴)) = ((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴)))))
104103cnveqd 5836 . . . . . . . . . . . . . . 15 (πœ‘ β†’ β—‘( ≀ ∩ (𝐴 Γ— 𝐴)) = β—‘((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴)))))
105104fveq2d 6851 . . . . . . . . . . . . . 14 (πœ‘ β†’ (ordTopβ€˜β—‘( ≀ ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜β—‘((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))))
106103fveq2d 6851 . . . . . . . . . . . . . 14 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜((leβ€˜(𝐾 β†Ύs 𝐴)) ∩ ((Baseβ€˜(𝐾 β†Ύs 𝐴)) Γ— (Baseβ€˜(𝐾 β†Ύs 𝐴))))))
10793, 105, 1063eqtr4d 2787 . . . . . . . . . . . . 13 (πœ‘ β†’ (ordTopβ€˜β—‘( ≀ ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
108 cnvin 6102 . . . . . . . . . . . . . . 15 β—‘( ≀ ∩ (𝐴 Γ— 𝐴)) = (β—‘ ≀ ∩ β—‘(𝐴 Γ— 𝐴))
109 cnvxp 6114 . . . . . . . . . . . . . . . 16 β—‘(𝐴 Γ— 𝐴) = (𝐴 Γ— 𝐴)
110109ineq2i 4174 . . . . . . . . . . . . . . 15 (β—‘ ≀ ∩ β—‘(𝐴 Γ— 𝐴)) = (β—‘ ≀ ∩ (𝐴 Γ— 𝐴))
111108, 110eqtri 2765 . . . . . . . . . . . . . 14 β—‘( ≀ ∩ (𝐴 Γ— 𝐴)) = (β—‘ ≀ ∩ (𝐴 Γ— 𝐴))
112111fveq2i 6850 . . . . . . . . . . . . 13 (ordTopβ€˜β—‘( ≀ ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(β—‘ ≀ ∩ (𝐴 Γ— 𝐴)))
113107, 112eqtr3di 2792 . . . . . . . . . . . 12 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) = (ordTopβ€˜(β—‘ ≀ ∩ (𝐴 Γ— 𝐴))))
114113eleq2d 2824 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(β—‘ ≀ ∩ (𝐴 Γ— 𝐴)))))
11587, 114raleqbidv 3322 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀◑ ≀ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜(β—‘ ≀ ∩ (𝐴 Γ— 𝐴)))))
11679, 115mpbird 257 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
117 ralunb 4156 . . . . . . . . 9 (βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ (βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∧ βˆ€π‘£ ∈ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴)))))
11856, 116, 117sylanbrc 584 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
119 ralunb 4156 . . . . . . . 8 (βˆ€π‘£ ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ (βˆ€π‘£ ∈ {𝐡} (𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∧ βˆ€π‘£ ∈ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴)))))
12054, 118, 119sylanbrc 584 . . . . . . 7 (πœ‘ β†’ βˆ€π‘£ ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
121 eqid 2737 . . . . . . . 8 (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴))
122121fmpt 7063 . . . . . . 7 (βˆ€π‘£ ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))(𝑣 ∩ 𝐴) ∈ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ↔ (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)):({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))⟢(ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
123120, 122sylib 217 . . . . . 6 (πœ‘ β†’ (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)):({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀})))⟢(ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
124123frnd 6681 . . . . 5 (πœ‘ β†’ ran (𝑣 ∈ ({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) ↦ (𝑣 ∩ 𝐴)) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
12537, 124eqsstrd 3987 . . . 4 (πœ‘ β†’ (({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
126 tgfiss 22357 . . . 4 (((ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) ∈ Top ∧ (({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴)))) β†’ (topGenβ€˜(fiβ€˜(({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴))) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
12730, 125, 126syl2anc 585 . . 3 (πœ‘ β†’ (topGenβ€˜(fiβ€˜(({𝐡} βˆͺ (ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑀 ≀ 𝑧}) βˆͺ ran (𝑧 ∈ 𝐡 ↦ {𝑀 ∈ 𝐡 ∣ Β¬ 𝑧 ≀ 𝑀}))) β†Ύt 𝐴))) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
12824, 127eqsstrd 3987 . 2 (πœ‘ β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) βŠ† (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))))
1299, 128eqssd 3966 1 (πœ‘ β†’ (ordTopβ€˜( ≀ ∩ (𝐴 Γ— 𝐴))) = ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  {crab 3410  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  {csn 4591  βˆͺ cuni 4870   class class class wbr 5110   ↦ cmpt 5193   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638  ran crn 5639  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  ficfi 9353  Basecbs 17090   β†Ύs cress 17119  lecple 17147   β†Ύt crest 17309  topGenctg 17326  ordTopcordt 17388  ODualcodu 18182   Proset cproset 18189  Posetcpo 18203  Tosetctos 18312  Topctop 22258  TopOnctopon 22275  TopBasesctb 22311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fi 9354  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-dec 12626  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-ple 17160  df-rest 17311  df-topgen 17332  df-ordt 17390  df-odu 18183  df-proset 18191  df-poset 18209  df-toset 18313  df-top 22259  df-topon 22276  df-bases 22312
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator