This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtrest2

Description: An interval-closed set A 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 RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrest2.1 ⊢ 𝑋 = dom 𝑅
ordtrest2.2 ⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
ordtrest2.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
ordtrest2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
Assertion ordtrest2 ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ordtrest2.1 ⊢ 𝑋 = dom 𝑅
2 ordtrest2.2 ⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
3 ordtrest2.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4 ordtrest2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
5 tsrps ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
6 2 5 syl ⊢ ( 𝜑 → 𝑅 ∈ PosetRel )
7 2 dmexd ⊢ ( 𝜑 → dom 𝑅 ∈ V )
8 1 7 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ V )
9 8 3 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
10 ordtrest ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ V ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
11 6 9 10 syl2anc ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )
12 eqid ⊢ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) = ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } )
13 eqid ⊢ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } )
14 1 12 13 ordtval ⊢ ( 𝑅 ∈ TosetRel → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) )
15 2 14 syl ⊢ ( 𝜑 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) )
16 15 oveq1d ⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾t 𝐴 ) )
17 fibas ⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ∈ TopBases
18 tgrest ⊢ ( ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ∈ TopBases ∧ 𝐴 ∈ V ) → ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾t 𝐴 ) )
19 17 9 18 sylancr ⊢ ( 𝜑 → ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾t 𝐴 ) )
20 16 19 eqtr4d ⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) = ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾t 𝐴 ) ) )
21 firest ⊢ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ) = ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾t 𝐴 )
22 21 fveq2i ⊢ ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ) ) = ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾t 𝐴 ) )
23 20 22 eqtr4di ⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) = ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ) ) )
24 inex1g ⊢ ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
25 2 24 syl ⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
26 ordttop ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
27 25 26 syl ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
28 1 12 13 ordtuni ⊢ ( 𝑅 ∈ TosetRel → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) )
29 2 28 syl ⊢ ( 𝜑 → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) )
30 29 8 eqeltrrd ⊢ ( 𝜑 → ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
31 uniexb ⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
32 30 31 sylibr ⊢ ( 𝜑 → ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
33 restval ⊢ ( ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V ∧ 𝐴 ∈ V ) → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
34 32 9 33 syl2anc ⊢ ( 𝜑 → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
35 sseqin2 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
36 3 35 sylib ⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
37 eqid ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) )
38 37 ordttopon ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
39 25 38 syl ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
40 1 psssdm ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
41 6 3 40 syl2anc ⊢ ( 𝜑 → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
42 41 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( TopOn ‘ 𝐴 ) )
43 39 42 eleqtrd ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) )
44 toponmax ⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
45 43 44 syl ⊢ ( 𝜑 → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
46 36 45 eqeltrd ⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
47 elsni ⊢ ( 𝑣 ∈ { 𝑋 } → 𝑣 = 𝑋 )
48 47 ineq1d ⊢ ( 𝑣 ∈ { 𝑋 } → ( 𝑣 ∩ 𝐴 ) = ( 𝑋 ∩ 𝐴 ) )
49 48 eleq1d ⊢ ( 𝑣 ∈ { 𝑋 } → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑋 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
50 46 49 syl5ibrcom ⊢ ( 𝜑 → ( 𝑣 ∈ { 𝑋 } → ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
51 50 ralrimiv ⊢ ( 𝜑 → ∀ 𝑣 ∈ { 𝑋 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
52 1 2 3 4 ordtrest2lem ⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
53 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
54 cnvtsr ⊢ ( 𝑅 ∈ TosetRel → ◡ 𝑅 ∈ TosetRel )
55 2 54 syl ⊢ ( 𝜑 → ◡ 𝑅 ∈ TosetRel )
56 1 psrn ⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 )
57 6 56 syl ⊢ ( 𝜑 → 𝑋 = ran 𝑅 )
58 3 57 sseqtrd ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝑅 )
59 57 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑋 = ran 𝑅 )
60 59 rabeqdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } )
61 vex ⊢ 𝑦 ∈ V
62 vex ⊢ 𝑧 ∈ V
63 61 62 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
64 vex ⊢ 𝑥 ∈ V
65 62 64 brcnv ⊢ ( 𝑧 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑧 )
66 63 65 anbi12ci ⊢ ( ( 𝑦 ◡ 𝑅 𝑧 ∧ 𝑧 ◡ 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) )
67 66 rabbii ⊢ { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ◡ 𝑅 𝑧 ∧ 𝑧 ◡ 𝑅 𝑥 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) }
68 60 67 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ◡ 𝑅 𝑧 ∧ 𝑧 ◡ 𝑅 𝑥 ) } )
69 68 4 eqsstrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ◡ 𝑅 𝑧 ∧ 𝑧 ◡ 𝑅 𝑥 ) } ⊆ 𝐴 )
70 69 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ◡ 𝑅 𝑧 ∧ 𝑧 ◡ 𝑅 𝑥 ) } ⊆ 𝐴 )
71 53 55 58 70 ordtrest2lem ⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ◡ 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
72 vex ⊢ 𝑤 ∈ V
73 72 62 brcnv ⊢ ( 𝑤 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑤 )
74 73 bicomi ⊢ ( 𝑧 𝑅 𝑤 ↔ 𝑤 ◡ 𝑅 𝑧 )
75 74 a1i ⊢ ( 𝜑 → ( 𝑧 𝑅 𝑤 ↔ 𝑤 ◡ 𝑅 𝑧 ) )
76 75 notbid ⊢ ( 𝜑 → ( ¬ 𝑧 𝑅 𝑤 ↔ ¬ 𝑤 ◡ 𝑅 𝑧 ) )
77 57 76 rabeqbidv ⊢ ( 𝜑 → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } = { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ◡ 𝑅 𝑧 } )
78 57 77 mpteq12dv ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ◡ 𝑅 𝑧 } ) )
79 78 rneqd ⊢ ( 𝜑 → ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ◡ 𝑅 𝑧 } ) )
80 psss ⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )
81 6 80 syl ⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )
82 ordtcnv ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel → ( ordTop ‘ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
83 81 82 syl ⊢ ( 𝜑 → ( ordTop ‘ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
84 cnvin ⊢ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ 𝑅 ∩ ◡ ( 𝐴 × 𝐴 ) )
85 cnvxp ⊢ ◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 )
86 85 ineq2i ⊢ ( ◡ 𝑅 ∩ ◡ ( 𝐴 × 𝐴 ) ) = ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) )
87 84 86 eqtri ⊢ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) )
88 87 fveq2i ⊢ ( ordTop ‘ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
89 83 88 eqtr3di ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
90 89 eleq2d ⊢ ( 𝜑 → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
91 79 90 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑣 ∈ ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ◡ 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
92 71 91 mpbird ⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
93 ralunb ⊢ ( ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
94 52 92 93 sylanbrc ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
95 ralunb ⊢ ( ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ { 𝑋 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
96 51 94 95 sylanbrc ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
97 eqid ⊢ ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) = ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) )
98 97 fmpt ⊢ ( ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
99 96 98 sylib ⊢ ( 𝜑 → ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
100 99 frnd ⊢ ( 𝜑 → ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
101 34 100 eqsstrd ⊢ ( 𝜑 → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
102 tgfiss ⊢ ( ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ∧ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) → ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
103 27 101 102 syl2anc ⊢ ( 𝜑 → ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
104 23 103 eqsstrd ⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
105 11 104 eqssd ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ 𝑅 ) ↾t 𝐴 ) )