Metamath Proof Explorer

Theorem ordtrest

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)

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

Proof

Step Hyp Ref Expression
1 inex1g ⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
2 1 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
3 eqid ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) )
4 eqid ⊢ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
5 eqid ⊢ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
6 3 4 5 ordtval ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( topGen ‘ ( fi ‘ ( { dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) )
7 2 6 syl ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( topGen ‘ ( fi ‘ ( { dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) )
8 ordttop ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Top )
9 resttop ⊢ ( ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) ∈ Top )
10 8 9 sylan ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) ∈ Top )
11 eqid ⊢ dom 𝑅 = dom 𝑅
12 11 psssdm2 ⊢ ( 𝑅 ∈ PosetRel → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( dom 𝑅 ∩ 𝐴 ) )
13 12 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( dom 𝑅 ∩ 𝐴 ) )
14 8 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ordTop ‘ 𝑅 ) ∈ Top )
15 simpr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
16 11 ordttopon ⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
17 16 adantr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
18 toponmax ⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) → dom 𝑅 ∈ ( ordTop ‘ 𝑅 ) )
19 17 18 syl ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → dom 𝑅 ∈ ( ordTop ‘ 𝑅 ) )
20 elrestr ⊢ ( ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ dom 𝑅 ∈ ( ordTop ‘ 𝑅 ) ) → ( dom 𝑅 ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
21 14 15 19 20 syl3anc ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( dom 𝑅 ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
22 13 21 eqeltrd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
23 22 snssd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → { dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
24 13 rabeqdv ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
25 13 24 mpteq12dv ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) )
26 25 rneqd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ran ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) )
27 inrab2 ⊢ ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 𝑅 𝑥 }
28 simpr ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) )
29 28 elin2d ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
30 simpr ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) )
31 30 elin2d ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
32 31 adantr ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
33 brinxp ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
34 29 32 33 syl2anc ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
35 34 notbid ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
36 35 rabbidva ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
37 27 36 syl5eq ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
38 14 adantr ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( ordTop ‘ 𝑅 ) ∈ Top )
39 15 adantr ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
40 simpl ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → 𝑅 ∈ PosetRel )
41 elinel1 ⊢ ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) → 𝑥 ∈ dom 𝑅 )
42 11 ordtopn1 ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
43 40 41 42 syl2an ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )
44 elrestr ⊢ ( ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
45 38 39 43 44 syl3anc ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
46 37 45 eqeltrrd ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
47 46 fmpttd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) : ( dom 𝑅 ∩ 𝐴 ) ⟶ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
48 47 frnd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
49 26 48 eqsstrd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
50 13 rabeqdv ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
51 13 50 mpteq12dv ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) )
52 51 rneqd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ran ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) )
53 inrab2 ⊢ ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 𝑅 𝑦 }
54 brinxp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
55 32 29 54 syl2anc ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
56 55 notbid ⊢ ( ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
57 56 rabbidva ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 𝑅 𝑦 } = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
58 53 57 syl5eq ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
59 11 ordtopn2 ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) )
60 40 41 59 syl2an ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) )
61 elrestr ⊢ ( ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ 𝐴 ∈ 𝑉 ∧ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ ( ordTop ‘ 𝑅 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
62 38 39 60 61 syl3anc ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
63 58 62 eqeltrrd ⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ∈ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
64 63 fmpttd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) : ( dom 𝑅 ∩ 𝐴 ) ⟶ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
65 64 frnd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ ( dom 𝑅 ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom 𝑅 ∩ 𝐴 ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
66 52 65 eqsstrd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
67 49 66 unssd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
68 23 67 unssd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( { dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
69 tgfiss ⊢ ( ( ( ( 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 ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( fi ‘ ( { dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
71 7 70 eqsstrd ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉 ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )