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 𝐴 ) )