ordthmeolem

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

Proof

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

Metamath Proof Explorer

Theorem ordthmeolem

Proof