# 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 ${⊢}{X}=\mathrm{dom}{R}$
ordtrest2.2 ${⊢}{\phi }\to {R}\in \mathrm{TosetRel}$
ordtrest2.3 ${⊢}{\phi }\to {A}\subseteq {X}$
ordtrest2.4 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left\{{z}\in {X}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}\subseteq {A}$
Assertion ordtrest2 ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)=\mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}$

### Proof

Step Hyp Ref Expression
1 ordtrest2.1 ${⊢}{X}=\mathrm{dom}{R}$
2 ordtrest2.2 ${⊢}{\phi }\to {R}\in \mathrm{TosetRel}$
3 ordtrest2.3 ${⊢}{\phi }\to {A}\subseteq {X}$
4 ordtrest2.4 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left\{{z}\in {X}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}\subseteq {A}$
5 tsrps ${⊢}{R}\in \mathrm{TosetRel}\to {R}\in \mathrm{PosetRel}$
6 2 5 syl ${⊢}{\phi }\to {R}\in \mathrm{PosetRel}$
7 2 dmexd ${⊢}{\phi }\to \mathrm{dom}{R}\in \mathrm{V}$
8 1 7 eqeltrid ${⊢}{\phi }\to {X}\in \mathrm{V}$
9 8 3 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
10 ordtrest ${⊢}\left({R}\in \mathrm{PosetRel}\wedge {A}\in \mathrm{V}\right)\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\subseteq \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}$
11 6 9 10 syl2anc ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\subseteq \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}$
12 eqid ${⊢}\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)=\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)$
13 eqid ${⊢}\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)=\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)$
14 1 12 13 ordtval ${⊢}{R}\in \mathrm{TosetRel}\to \mathrm{ordTop}\left({R}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\right)$
15 2 14 syl ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\right)$
16 15 oveq1d ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\right){↾}_{𝑡}{A}$
17 fibas ${⊢}\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\in \mathrm{TopBases}$
18 tgrest ${⊢}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\in \mathrm{TopBases}\wedge {A}\in \mathrm{V}\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\right){↾}_{𝑡}{A}$
19 17 9 18 sylancr ${⊢}{\phi }\to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\right){↾}_{𝑡}{A}$
20 16 19 eqtr4d ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)$
21 firest ${⊢}\mathrm{fi}\left(\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)=\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}$
22 21 fveq2i ${⊢}\mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)$
23 20 22 syl6eqr ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}=\mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)\right)$
24 inex1g ${⊢}{R}\in \mathrm{TosetRel}\to {R}\cap \left({A}×{A}\right)\in \mathrm{V}$
25 2 24 syl ${⊢}{\phi }\to {R}\cap \left({A}×{A}\right)\in \mathrm{V}$
26 ordttop ${⊢}{R}\cap \left({A}×{A}\right)\in \mathrm{V}\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{Top}$
27 25 26 syl ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{Top}$
28 1 12 13 ordtuni ${⊢}{R}\in \mathrm{TosetRel}\to {X}=\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)$
29 2 28 syl ${⊢}{\phi }\to {X}=\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)$
30 29 8 eqeltrrd ${⊢}{\phi }\to \bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\in \mathrm{V}$
31 uniexb ${⊢}\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\in \mathrm{V}↔\bigcup \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\in \mathrm{V}$
32 30 31 sylibr ${⊢}{\phi }\to \left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\in \mathrm{V}$
33 restval ${⊢}\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}=\mathrm{ran}\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right)$
34 32 9 33 syl2anc ${⊢}{\phi }\to \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}=\mathrm{ran}\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right)$
35 sseqin2 ${⊢}{A}\subseteq {X}↔{X}\cap {A}={A}$
36 3 35 sylib ${⊢}{\phi }\to {X}\cap {A}={A}$
37 eqid ${⊢}\mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)=\mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)$
38 37 ordttopon ${⊢}{R}\cap \left({A}×{A}\right)\in \mathrm{V}\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{TopOn}\left(\mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)\right)$
39 25 38 syl ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{TopOn}\left(\mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)\right)$
40 1 psssdm ${⊢}\left({R}\in \mathrm{PosetRel}\wedge {A}\subseteq {X}\right)\to \mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)={A}$
41 6 3 40 syl2anc ${⊢}{\phi }\to \mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)={A}$
42 41 fveq2d ${⊢}{\phi }\to \mathrm{TopOn}\left(\mathrm{dom}\left({R}\cap \left({A}×{A}\right)\right)\right)=\mathrm{TopOn}\left({A}\right)$
43 39 42 eleqtrd ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{TopOn}\left({A}\right)$
44 toponmax ${⊢}\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{TopOn}\left({A}\right)\to {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
45 43 44 syl ${⊢}{\phi }\to {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
46 36 45 eqeltrd ${⊢}{\phi }\to {X}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
47 elsni ${⊢}{v}\in \left\{{X}\right\}\to {v}={X}$
48 47 ineq1d ${⊢}{v}\in \left\{{X}\right\}\to {v}\cap {A}={X}\cap {A}$
49 48 eleq1d ${⊢}{v}\in \left\{{X}\right\}\to \left({v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔{X}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\right)$
50 46 49 syl5ibrcom ${⊢}{\phi }\to \left({v}\in \left\{{X}\right\}\to {v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\right)$
51 50 ralrimiv ${⊢}{\phi }\to \forall {v}\in \left\{{X}\right\}\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
52 1 2 3 4 ordtrest2lem ${⊢}{\phi }\to \forall {v}\in \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
53 df-rn ${⊢}\mathrm{ran}{R}=\mathrm{dom}{{R}}^{-1}$
54 cnvtsr ${⊢}{R}\in \mathrm{TosetRel}\to {{R}}^{-1}\in \mathrm{TosetRel}$
55 2 54 syl ${⊢}{\phi }\to {{R}}^{-1}\in \mathrm{TosetRel}$
56 1 psrn ${⊢}{R}\in \mathrm{PosetRel}\to {X}=\mathrm{ran}{R}$
57 6 56 syl ${⊢}{\phi }\to {X}=\mathrm{ran}{R}$
58 3 57 sseqtrd ${⊢}{\phi }\to {A}\subseteq \mathrm{ran}{R}$
59 57 adantr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to {X}=\mathrm{ran}{R}$
60 59 rabeqdv ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left\{{z}\in {X}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}=\left\{{z}\in \mathrm{ran}{R}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}$
61 vex ${⊢}{y}\in \mathrm{V}$
62 vex ${⊢}{z}\in \mathrm{V}$
63 61 62 brcnv ${⊢}{y}{{R}}^{-1}{z}↔{z}{R}{y}$
64 vex ${⊢}{x}\in \mathrm{V}$
65 62 64 brcnv ${⊢}{z}{{R}}^{-1}{x}↔{x}{R}{z}$
66 63 65 anbi12ci ${⊢}\left({y}{{R}}^{-1}{z}\wedge {z}{{R}}^{-1}{x}\right)↔\left({x}{R}{z}\wedge {z}{R}{y}\right)$
67 66 rabbii ${⊢}\left\{{z}\in \mathrm{ran}{R}|\left({y}{{R}}^{-1}{z}\wedge {z}{{R}}^{-1}{x}\right)\right\}=\left\{{z}\in \mathrm{ran}{R}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}$
68 60 67 syl6eqr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left\{{z}\in {X}|\left({x}{R}{z}\wedge {z}{R}{y}\right)\right\}=\left\{{z}\in \mathrm{ran}{R}|\left({y}{{R}}^{-1}{z}\wedge {z}{{R}}^{-1}{x}\right)\right\}$
69 68 4 eqsstrrd ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left\{{z}\in \mathrm{ran}{R}|\left({y}{{R}}^{-1}{z}\wedge {z}{{R}}^{-1}{x}\right)\right\}\subseteq {A}$
70 69 ancom2s ${⊢}\left({\phi }\wedge \left({y}\in {A}\wedge {x}\in {A}\right)\right)\to \left\{{z}\in \mathrm{ran}{R}|\left({y}{{R}}^{-1}{z}\wedge {z}{{R}}^{-1}{x}\right)\right\}\subseteq {A}$
71 53 55 58 70 ordtrest2lem ${⊢}{\phi }\to \forall {v}\in \mathrm{ran}\left({z}\in \mathrm{ran}{R}⟼\left\{{w}\in \mathrm{ran}{R}|¬{w}{{R}}^{-1}{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({{R}}^{-1}\cap \left({A}×{A}\right)\right)$
72 vex ${⊢}{w}\in \mathrm{V}$
73 72 62 brcnv ${⊢}{w}{{R}}^{-1}{z}↔{z}{R}{w}$
74 73 bicomi ${⊢}{z}{R}{w}↔{w}{{R}}^{-1}{z}$
75 74 a1i ${⊢}{\phi }\to \left({z}{R}{w}↔{w}{{R}}^{-1}{z}\right)$
76 75 notbid ${⊢}{\phi }\to \left(¬{z}{R}{w}↔¬{w}{{R}}^{-1}{z}\right)$
77 57 76 rabeqbidv ${⊢}{\phi }\to \left\{{w}\in {X}|¬{z}{R}{w}\right\}=\left\{{w}\in \mathrm{ran}{R}|¬{w}{{R}}^{-1}{z}\right\}$
78 57 77 mpteq12dv ${⊢}{\phi }\to \left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)=\left({z}\in \mathrm{ran}{R}⟼\left\{{w}\in \mathrm{ran}{R}|¬{w}{{R}}^{-1}{z}\right\}\right)$
79 78 rneqd ${⊢}{\phi }\to \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)=\mathrm{ran}\left({z}\in \mathrm{ran}{R}⟼\left\{{w}\in \mathrm{ran}{R}|¬{w}{{R}}^{-1}{z}\right\}\right)$
80 cnvin ${⊢}{\left({R}\cap \left({A}×{A}\right)\right)}^{-1}={{R}}^{-1}\cap {\left({A}×{A}\right)}^{-1}$
81 cnvxp ${⊢}{\left({A}×{A}\right)}^{-1}={A}×{A}$
82 81 ineq2i ${⊢}{{R}}^{-1}\cap {\left({A}×{A}\right)}^{-1}={{R}}^{-1}\cap \left({A}×{A}\right)$
83 80 82 eqtri ${⊢}{\left({R}\cap \left({A}×{A}\right)\right)}^{-1}={{R}}^{-1}\cap \left({A}×{A}\right)$
84 83 fveq2i ${⊢}\mathrm{ordTop}\left({\left({R}\cap \left({A}×{A}\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({{R}}^{-1}\cap \left({A}×{A}\right)\right)$
85 psss ${⊢}{R}\in \mathrm{PosetRel}\to {R}\cap \left({A}×{A}\right)\in \mathrm{PosetRel}$
86 6 85 syl ${⊢}{\phi }\to {R}\cap \left({A}×{A}\right)\in \mathrm{PosetRel}$
87 ordtcnv ${⊢}{R}\cap \left({A}×{A}\right)\in \mathrm{PosetRel}\to \mathrm{ordTop}\left({\left({R}\cap \left({A}×{A}\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
88 86 87 syl ${⊢}{\phi }\to \mathrm{ordTop}\left({\left({R}\cap \left({A}×{A}\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
89 84 88 syl5reqr ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)=\mathrm{ordTop}\left({{R}}^{-1}\cap \left({A}×{A}\right)\right)$
90 89 eleq2d ${⊢}{\phi }\to \left({v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔{v}\cap {A}\in \mathrm{ordTop}\left({{R}}^{-1}\cap \left({A}×{A}\right)\right)\right)$
91 79 90 raleqbidv ${⊢}{\phi }\to \left(\forall {v}\in \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔\forall {v}\in \mathrm{ran}\left({z}\in \mathrm{ran}{R}⟼\left\{{w}\in \mathrm{ran}{R}|¬{w}{{R}}^{-1}{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({{R}}^{-1}\cap \left({A}×{A}\right)\right)\right)$
92 71 91 mpbird ${⊢}{\phi }\to \forall {v}\in \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
93 ralunb ${⊢}\forall {v}\in \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔\left(\forall {v}\in \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\wedge \forall {v}\in \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\right)$
94 52 92 93 sylanbrc ${⊢}{\phi }\to \forall {v}\in \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
95 ralunb ${⊢}\forall {v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔\left(\forall {v}\in \left\{{X}\right\}\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\wedge \forall {v}\in \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\right)$
96 51 94 95 sylanbrc ${⊢}{\phi }\to \forall {v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
97 eqid ${⊢}\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right)=\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right)$
98 97 fmpt ${⊢}\forall {v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{v}\cap {A}\in \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)↔\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right):\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)⟶\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
99 96 98 sylib ${⊢}{\phi }\to \left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right):\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)⟶\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
100 99 frnd ${⊢}{\phi }\to \mathrm{ran}\left({v}\in \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right)⟼{v}\cap {A}\right)\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
101 34 100 eqsstrd ${⊢}{\phi }\to \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
102 tgfiss ${⊢}\left(\mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\in \mathrm{Top}\wedge \left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)\right)\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
103 27 101 102 syl2anc ${⊢}{\phi }\to \mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{{X}\right\}\cup \left(\mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{w}{R}{z}\right\}\right)\cup \mathrm{ran}\left({z}\in {X}⟼\left\{{w}\in {X}|¬{z}{R}{w}\right\}\right)\right)\right){↾}_{𝑡}{A}\right)\right)\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
104 23 103 eqsstrd ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}\subseteq \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)$
105 11 104 eqssd ${⊢}{\phi }\to \mathrm{ordTop}\left({R}\cap \left({A}×{A}\right)\right)=\mathrm{ordTop}\left({R}\right){↾}_{𝑡}{A}$