# Metamath Proof Explorer

## Theorem ordthmeolem

Description: Lemma for ordthmeo . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordthmeo.1 ${⊢}{X}=\mathrm{dom}{R}$
ordthmeo.2 ${⊢}{Y}=\mathrm{dom}{S}$
Assertion ordthmeolem ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {F}\in \left(\mathrm{ordTop}\left({R}\right)\mathrm{Cn}\mathrm{ordTop}\left({S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ordthmeo.1 ${⊢}{X}=\mathrm{dom}{R}$
2 ordthmeo.2 ${⊢}{Y}=\mathrm{dom}{S}$
3 isof1o ${⊢}{F}{Isom}_{{R},{S}}\left({X},{Y}\right)\to {F}:{X}\underset{1-1 onto}{⟶}{Y}$
4 3 3ad2ant3 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {F}:{X}\underset{1-1 onto}{⟶}{Y}$
5 f1of ${⊢}{F}:{X}\underset{1-1 onto}{⟶}{Y}\to {F}:{X}⟶{Y}$
6 4 5 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {F}:{X}⟶{Y}$
7 fimacnv ${⊢}{F}:{X}⟶{Y}\to {{F}}^{-1}\left[{Y}\right]={X}$
8 6 7 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {{F}}^{-1}\left[{Y}\right]={X}$
9 1 ordttopon ${⊢}{R}\in {V}\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
10 9 3ad2ant1 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)$
11 toponmax ${⊢}\mathrm{ordTop}\left({R}\right)\in \mathrm{TopOn}\left({X}\right)\to {X}\in \mathrm{ordTop}\left({R}\right)$
12 10 11 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {X}\in \mathrm{ordTop}\left({R}\right)$
13 8 12 eqeltrd ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {{F}}^{-1}\left[{Y}\right]\in \mathrm{ordTop}\left({R}\right)$
14 elsni ${⊢}{z}\in \left\{{Y}\right\}\to {z}={Y}$
15 14 imaeq2d ${⊢}{z}\in \left\{{Y}\right\}\to {{F}}^{-1}\left[{z}\right]={{F}}^{-1}\left[{Y}\right]$
16 15 eleq1d ${⊢}{z}\in \left\{{Y}\right\}\to \left({{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔{{F}}^{-1}\left[{Y}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
17 13 16 syl5ibrcom ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left({z}\in \left\{{Y}\right\}\to {{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
18 17 ralrimiv ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {z}\in \left\{{Y}\right\}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)$
19 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\subseteq \mathrm{dom}{F}$
20 f1odm ${⊢}{F}:{X}\underset{1-1 onto}{⟶}{Y}\to \mathrm{dom}{F}={X}$
21 4 20 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \mathrm{dom}{F}={X}$
22 21 adantr ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to \mathrm{dom}{F}={X}$
23 19 22 sseqtrid ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\subseteq {X}$
24 sseqin2 ${⊢}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\subseteq {X}↔{X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]$
25 23 24 sylib ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]$
26 4 ad2antrr ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {F}:{X}\underset{1-1 onto}{⟶}{Y}$
27 f1ofn ${⊢}{F}:{X}\underset{1-1 onto}{⟶}{Y}\to {F}Fn{X}$
28 26 27 syl ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {F}Fn{X}$
29 elpreima ${⊢}{F}Fn{X}\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\right)$
30 28 29 syl ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\right)$
31 simpr ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {z}\in {X}$
32 31 biantrurd ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\right)$
33 6 adantr ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {F}:{X}⟶{Y}$
34 33 ffvelrnda ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {F}\left({z}\right)\in {Y}$
35 breq1 ${⊢}{y}={F}\left({z}\right)\to \left({y}{S}{x}↔{F}\left({z}\right){S}{x}\right)$
36 35 notbid ${⊢}{y}={F}\left({z}\right)\to \left(¬{y}{S}{x}↔¬{F}\left({z}\right){S}{x}\right)$
37 36 elrab3 ${⊢}{F}\left({z}\right)\in {Y}\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}↔¬{F}\left({z}\right){S}{x}\right)$
38 34 37 syl ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}↔¬{F}\left({z}\right){S}{x}\right)$
39 simpll3 ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {F}{Isom}_{{R},{S}}\left({X},{Y}\right)$
40 f1ocnv ${⊢}{F}:{X}\underset{1-1 onto}{⟶}{Y}\to {{F}}^{-1}:{Y}\underset{1-1 onto}{⟶}{X}$
41 f1of ${⊢}{{F}}^{-1}:{Y}\underset{1-1 onto}{⟶}{X}\to {{F}}^{-1}:{Y}⟶{X}$
42 4 40 41 3syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {{F}}^{-1}:{Y}⟶{X}$
43 42 ffvelrnda ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left({x}\right)\in {X}$
44 43 adantr ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {{F}}^{-1}\left({x}\right)\in {X}$
45 isorel ${⊢}\left({F}{Isom}_{{R},{S}}\left({X},{Y}\right)\wedge \left({z}\in {X}\wedge {{F}}^{-1}\left({x}\right)\in {X}\right)\right)\to \left({z}{R}{{F}}^{-1}\left({x}\right)↔{F}\left({z}\right){S}{F}\left({{F}}^{-1}\left({x}\right)\right)\right)$
46 39 31 44 45 syl12anc ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}{R}{{F}}^{-1}\left({x}\right)↔{F}\left({z}\right){S}{F}\left({{F}}^{-1}\left({x}\right)\right)\right)$
47 f1ocnvfv2 ${⊢}\left({F}:{X}\underset{1-1 onto}{⟶}{Y}\wedge {x}\in {Y}\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right)={x}$
48 4 47 sylan ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right)={x}$
49 48 adantr ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to {F}\left({{F}}^{-1}\left({x}\right)\right)={x}$
50 49 breq2d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right){S}{F}\left({{F}}^{-1}\left({x}\right)\right)↔{F}\left({z}\right){S}{x}\right)$
51 46 50 bitrd ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}{R}{{F}}^{-1}\left({x}\right)↔{F}\left({z}\right){S}{x}\right)$
52 51 notbid ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left(¬{z}{R}{{F}}^{-1}\left({x}\right)↔¬{F}\left({z}\right){S}{x}\right)$
53 38 52 bitr4d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{y}{S}{x}\right\}↔¬{z}{R}{{F}}^{-1}\left({x}\right)\right)$
54 30 32 53 3bitr2d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]↔¬{z}{R}{{F}}^{-1}\left({x}\right)\right)$
55 54 rabbi2dva ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]=\left\{{z}\in {X}|¬{z}{R}{{F}}^{-1}\left({x}\right)\right\}$
56 25 55 eqtr3d ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]=\left\{{z}\in {X}|¬{z}{R}{{F}}^{-1}\left({x}\right)\right\}$
57 simpl1 ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {R}\in {V}$
58 1 ordtopn1 ${⊢}\left({R}\in {V}\wedge {{F}}^{-1}\left({x}\right)\in {X}\right)\to \left\{{z}\in {X}|¬{z}{R}{{F}}^{-1}\left({x}\right)\right\}\in \mathrm{ordTop}\left({R}\right)$
59 57 43 58 syl2anc ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to \left\{{z}\in {X}|¬{z}{R}{{F}}^{-1}\left({x}\right)\right\}\in \mathrm{ordTop}\left({R}\right)$
60 56 59 eqeltrd ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\in \mathrm{ordTop}\left({R}\right)$
61 60 ralrimiva ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\in \mathrm{ordTop}\left({R}\right)$
62 dmexg ${⊢}{S}\in {W}\to \mathrm{dom}{S}\in \mathrm{V}$
63 2 62 eqeltrid ${⊢}{S}\in {W}\to {Y}\in \mathrm{V}$
64 63 3ad2ant2 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {Y}\in \mathrm{V}$
65 rabexg ${⊢}{Y}\in \mathrm{V}\to \left\{{y}\in {Y}|¬{y}{S}{x}\right\}\in \mathrm{V}$
66 64 65 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left\{{y}\in {Y}|¬{y}{S}{x}\right\}\in \mathrm{V}$
67 66 ralrimivw ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\in \mathrm{V}$
68 eqid ${⊢}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)=\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)$
69 imaeq2 ${⊢}{z}=\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\to {{F}}^{-1}\left[{z}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]$
70 69 eleq1d ${⊢}{z}=\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\to \left({{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
71 68 70 ralrnmptw ${⊢}\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\in \mathrm{V}\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
72 67 71 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
73 61 72 mpbird ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)$
74 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\subseteq \mathrm{dom}{F}$
75 74 22 sseqtrid ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\subseteq {X}$
76 sseqin2 ${⊢}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\subseteq {X}↔{X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]$
77 75 76 sylib ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]$
78 elpreima ${⊢}{F}Fn{X}\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)$
79 28 78 syl ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)$
80 31 biantrurd ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}↔\left({z}\in {X}\wedge {F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)$
81 breq2 ${⊢}{y}={F}\left({z}\right)\to \left({x}{S}{y}↔{x}{S}{F}\left({z}\right)\right)$
82 81 notbid ${⊢}{y}={F}\left({z}\right)\to \left(¬{x}{S}{y}↔¬{x}{S}{F}\left({z}\right)\right)$
83 82 elrab3 ${⊢}{F}\left({z}\right)\in {Y}\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}↔¬{x}{S}{F}\left({z}\right)\right)$
84 34 83 syl ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}↔¬{x}{S}{F}\left({z}\right)\right)$
85 isorel ${⊢}\left({F}{Isom}_{{R},{S}}\left({X},{Y}\right)\wedge \left({{F}}^{-1}\left({x}\right)\in {X}\wedge {z}\in {X}\right)\right)\to \left({{F}}^{-1}\left({x}\right){R}{z}↔{F}\left({{F}}^{-1}\left({x}\right)\right){S}{F}\left({z}\right)\right)$
86 39 44 31 85 syl12anc ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({{F}}^{-1}\left({x}\right){R}{z}↔{F}\left({{F}}^{-1}\left({x}\right)\right){S}{F}\left({z}\right)\right)$
87 49 breq1d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({{F}}^{-1}\left({x}\right)\right){S}{F}\left({z}\right)↔{x}{S}{F}\left({z}\right)\right)$
88 86 87 bitrd ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({{F}}^{-1}\left({x}\right){R}{z}↔{x}{S}{F}\left({z}\right)\right)$
89 88 notbid ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left(¬{{F}}^{-1}\left({x}\right){R}{z}↔¬{x}{S}{F}\left({z}\right)\right)$
90 84 89 bitr4d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({F}\left({z}\right)\in \left\{{y}\in {Y}|¬{x}{S}{y}\right\}↔¬{{F}}^{-1}\left({x}\right){R}{z}\right)$
91 79 80 90 3bitr2d ${⊢}\left(\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\wedge {z}\in {X}\right)\to \left({z}\in {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]↔¬{{F}}^{-1}\left({x}\right){R}{z}\right)$
92 91 rabbi2dva ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {X}\cap {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]=\left\{{z}\in {X}|¬{{F}}^{-1}\left({x}\right){R}{z}\right\}$
93 77 92 eqtr3d ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]=\left\{{z}\in {X}|¬{{F}}^{-1}\left({x}\right){R}{z}\right\}$
94 1 ordtopn2 ${⊢}\left({R}\in {V}\wedge {{F}}^{-1}\left({x}\right)\in {X}\right)\to \left\{{z}\in {X}|¬{{F}}^{-1}\left({x}\right){R}{z}\right\}\in \mathrm{ordTop}\left({R}\right)$
95 57 43 94 syl2anc ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to \left\{{z}\in {X}|¬{{F}}^{-1}\left({x}\right){R}{z}\right\}\in \mathrm{ordTop}\left({R}\right)$
96 93 95 eqeltrd ${⊢}\left(\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\wedge {x}\in {Y}\right)\to {{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\in \mathrm{ordTop}\left({R}\right)$
97 96 ralrimiva ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\in \mathrm{ordTop}\left({R}\right)$
98 rabexg ${⊢}{Y}\in \mathrm{V}\to \left\{{y}\in {Y}|¬{x}{S}{y}\right\}\in \mathrm{V}$
99 64 98 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left\{{y}\in {Y}|¬{x}{S}{y}\right\}\in \mathrm{V}$
100 99 ralrimivw ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\in \mathrm{V}$
101 eqid ${⊢}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)=\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)$
102 imaeq2 ${⊢}{z}=\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\to {{F}}^{-1}\left[{z}\right]={{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]$
103 102 eleq1d ${⊢}{z}=\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\to \left({{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
104 101 103 ralrnmptw ${⊢}\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\in \mathrm{V}\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
105 100 104 syl ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\forall {x}\in {Y}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
106 97 105 mpbird ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)$
107 ralunb ${⊢}\forall {z}\in \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\left(\forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\wedge \forall {z}\in \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
108 73 106 107 sylanbrc ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {z}\in \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)$
109 ralunb ${⊢}\forall {z}\in \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)↔\left(\forall {z}\in \left\{{Y}\right\}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\wedge \forall {z}\in \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\right)$
110 18 108 109 sylanbrc ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \forall {z}\in \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)$
111 eqid ${⊢}\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)=\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)$
112 eqid ${⊢}\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)=\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)$
113 2 111 112 ordtuni ${⊢}{S}\in {W}\to {Y}=\bigcup \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)$
114 113 63 eqeltrrd ${⊢}{S}\in {W}\to \bigcup \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\in \mathrm{V}$
115 uniexb ${⊢}\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\in \mathrm{V}↔\bigcup \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\in \mathrm{V}$
116 114 115 sylibr ${⊢}{S}\in {W}\to \left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\in \mathrm{V}$
117 116 3ad2ant2 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\in \mathrm{V}$
118 2 111 112 ordtval ${⊢}{S}\in {W}\to \mathrm{ordTop}\left({S}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\right)$
119 118 3ad2ant2 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \mathrm{ordTop}\left({S}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\right)$
120 2 ordttopon ${⊢}{S}\in {W}\to \mathrm{ordTop}\left({S}\right)\in \mathrm{TopOn}\left({Y}\right)$
121 120 3ad2ant2 ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \mathrm{ordTop}\left({S}\right)\in \mathrm{TopOn}\left({Y}\right)$
122 10 117 119 121 subbascn ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to \left({F}\in \left(\mathrm{ordTop}\left({R}\right)\mathrm{Cn}\mathrm{ordTop}\left({S}\right)\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in \left(\left\{{Y}\right\}\cup \left(\mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{y}{S}{x}\right\}\right)\cup \mathrm{ran}\left({x}\in {Y}⟼\left\{{y}\in {Y}|¬{x}{S}{y}\right\}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{ordTop}\left({R}\right)\right)\right)$
123 6 110 122 mpbir2and ${⊢}\left({R}\in {V}\wedge {S}\in {W}\wedge {F}{Isom}_{{R},{S}}\left({X},{Y}\right)\right)\to {F}\in \left(\mathrm{ordTop}\left({R}\right)\mathrm{Cn}\mathrm{ordTop}\left({S}\right)\right)$