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

Metamath Proof Explorer

Theorem ordthmeolem

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

Ref Expression
Hypotheses ordthmeo.1 ⊢ 𝑋 = dom 𝑅
ordthmeo.2 ⊢ 𝑌 = dom 𝑆
Assertion ordthmeolem ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Cn ( ordTop ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ordthmeo.1 ⊢ 𝑋 = dom 𝑅
2 ordthmeo.2 ⊢ 𝑌 = dom 𝑆
3 isof1o ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
4 3 3ad2ant3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
5 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
6 4 5 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
7 fimacnv ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = 𝑋 )
8 6 7 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ◡ 𝐹 “ 𝑌 ) = 𝑋 )
9 1 ordttopon ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )
10 9 3ad2ant1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )
11 toponmax ⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ ( ordTop ‘ 𝑅 ) )
12 10 11 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝑋 ∈ ( ordTop ‘ 𝑅 ) )
13 8 12 eqeltrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ◡ 𝐹 “ 𝑌 ) ∈ ( ordTop ‘ 𝑅 ) )
14 elsni ⊢ ( 𝑧 ∈ { 𝑌 } → 𝑧 = 𝑌 )
15 14 imaeq2d ⊢ ( 𝑧 ∈ { 𝑌 } → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ 𝑌 ) )
16 15 eleq1d ⊢ ( 𝑧 ∈ { 𝑌 } → ( ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ( ◡ 𝐹 “ 𝑌 ) ∈ ( ordTop ‘ 𝑅 ) ) )
17 13 16 syl5ibrcom ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( 𝑧 ∈ { 𝑌 } → ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ) )
18 17 ralrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑧 ∈ { 𝑌 } ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) )
19 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ⊆ dom 𝐹
20 f1odm ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → dom 𝐹 = 𝑋 )
21 4 20 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → dom 𝐹 = 𝑋 )
22 21 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → dom 𝐹 = 𝑋 )
23 19 22 sseqtrid ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ⊆ 𝑋 )
24 sseqin2 ⊢ ( ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ⊆ 𝑋 ↔ ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) )
25 23 24 sylib ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) )
26 4 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
27 f1ofn ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 Fn 𝑋 )
28 26 27 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
29 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) )
30 28 29 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) )
31 simpr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
32 31 biantrurd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) )
33 6 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
34 33 ffvelcdmda ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 )
35 breq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( 𝑦 𝑆 𝑥 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
36 35 notbid ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( ¬ 𝑦 𝑆 𝑥 ↔ ¬ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
37 36 elrab3 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ↔ ¬ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
38 34 37 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ↔ ¬ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
39 simpll3 ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) )
40 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
41 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
42 4 40 41 3syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
43 42 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
44 43 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
45 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) ) → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
46 39 31 44 45 syl12anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
47 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
48 4 47 sylan ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
49 48 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
50 49 breq2d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
51 46 50 bitrd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
52 51 notbid ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑧 ) 𝑆 𝑥 ) )
53 38 52 bitr4d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ↔ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ) )
54 30 32 53 3bitr2d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ↔ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) ) )
55 54 rabbi2dva ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ) = { 𝑧 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) } )
56 25 55 eqtr3d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) = { 𝑧 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) } )
57 simpl1 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ∈ 𝑉 )
58 1 ordtopn1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) → { 𝑧 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) } ∈ ( ordTop ‘ 𝑅 ) )
59 57 43 58 syl2anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → { 𝑧 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑥 ) } ∈ ( ordTop ‘ 𝑅 ) )
60 56 59 eqeltrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∈ ( ordTop ‘ 𝑅 ) )
61 60 ralrimiva ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∈ ( ordTop ‘ 𝑅 ) )
62 dmexg ⊢ ( 𝑆 ∈ 𝑊 → dom 𝑆 ∈ V )
63 2 62 eqeltrid ⊢ ( 𝑆 ∈ 𝑊 → 𝑌 ∈ V )
64 63 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝑌 ∈ V )
65 rabexg ⊢ ( 𝑌 ∈ V → { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ∈ V )
66 64 65 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ∈ V )
67 66 ralrimivw ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑥 ∈ 𝑌 { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ∈ V )
68 eqid ⊢ ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) = ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } )
69 imaeq2 ⊢ ( 𝑧 = { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) )
70 69 eleq1d ⊢ ( 𝑧 = { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } → ( ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
71 68 70 ralrnmptw ⊢ ( ∀ 𝑥 ∈ 𝑌 { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
72 67 71 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
73 61 72 mpbird ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) )
74 cnvimass ⊢ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ⊆ dom 𝐹
75 74 22 sseqtrid ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ⊆ 𝑋 )
76 sseqin2 ⊢ ( ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ⊆ 𝑋 ↔ ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) )
77 75 76 sylib ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) )
78 elpreima ⊢ ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) )
79 28 78 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) )
80 31 biantrurd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) )
81 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 𝑆 𝑦 ↔ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
82 81 notbid ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → ( ¬ 𝑥 𝑆 𝑦 ↔ ¬ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
83 82 elrab3 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑌 → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ↔ ¬ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
84 34 83 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ↔ ¬ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
85 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
86 39 44 31 85 syl12anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
87 49 breq1d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) 𝑆 ( 𝐹 ‘ 𝑧 ) ↔ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
88 86 87 bitrd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ↔ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
89 88 notbid ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ↔ ¬ 𝑥 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
90 84 89 bitr4d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ↔ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ) )
91 79 80 90 3bitr2d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ↔ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 ) )
92 91 rabbi2dva ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 ∩ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) = { 𝑧 ∈ 𝑋 ∣ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 } )
93 77 92 eqtr3d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) = { 𝑧 ∈ 𝑋 ∣ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 } )
94 1 ordtopn2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) → { 𝑧 ∈ 𝑋 ∣ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 } ∈ ( ordTop ‘ 𝑅 ) )
95 57 43 94 syl2anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → { 𝑧 ∈ 𝑋 ∣ ¬ ( ◡ 𝐹 ‘ 𝑥 ) 𝑅 𝑧 } ∈ ( ordTop ‘ 𝑅 ) )
96 93 95 eqeltrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ∈ ( ordTop ‘ 𝑅 ) )
97 96 ralrimiva ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ∈ ( ordTop ‘ 𝑅 ) )
98 rabexg ⊢ ( 𝑌 ∈ V → { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ∈ V )
99 64 98 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ∈ V )
100 99 ralrimivw ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑥 ∈ 𝑌 { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ∈ V )
101 eqid ⊢ ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) = ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } )
102 imaeq2 ⊢ ( 𝑧 = { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) )
103 102 eleq1d ⊢ ( 𝑧 = { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } → ( ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
104 101 103 ralrnmptw ⊢ ( ∀ 𝑥 ∈ 𝑌 { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
105 100 104 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑌 ( ◡ 𝐹 “ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ∈ ( ordTop ‘ 𝑅 ) ) )
106 97 105 mpbird ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) )
107 ralunb ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ) )
108 73 106 107 sylanbrc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) )
109 ralunb ⊢ ( ∀ 𝑧 ∈ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ↔ ( ∀ 𝑧 ∈ { 𝑌 } ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ∧ ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ) )
110 18 108 109 sylanbrc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ∀ 𝑧 ∈ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) )
111 eqid ⊢ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) = ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } )
112 eqid ⊢ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) = ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } )
113 2 111 112 ordtuni ⊢ ( 𝑆 ∈ 𝑊 → 𝑌 = ∪ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) )
114 113 63 eqeltrrd ⊢ ( 𝑆 ∈ 𝑊 → ∪ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ∈ V )
115 uniexb ⊢ ( ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ∈ V ↔ ∪ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ∈ V )
116 114 115 sylibr ⊢ ( 𝑆 ∈ 𝑊 → ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ∈ V )
117 116 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ∈ V )
118 2 111 112 ordtval ⊢ ( 𝑆 ∈ 𝑊 → ( ordTop ‘ 𝑆 ) = ( topGen ‘ ( fi ‘ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ) ) )
119 118 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ordTop ‘ 𝑆 ) = ( topGen ‘ ( fi ‘ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ) ) )
120 2 ordttopon ⊢ ( 𝑆 ∈ 𝑊 → ( ordTop ‘ 𝑆 ) ∈ ( TopOn ‘ 𝑌 ) )
121 120 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( ordTop ‘ 𝑆 ) ∈ ( TopOn ‘ 𝑌 ) )
122 10 117 119 121 subbascn ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ( 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Cn ( ordTop ‘ 𝑆 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ ( { 𝑌 } ∪ ( ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑦 𝑆 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝑌 ↦ { 𝑦 ∈ 𝑌 ∣ ¬ 𝑥 𝑆 𝑦 } ) ) ) ( ◡ 𝐹 “ 𝑧 ) ∈ ( ordTop ‘ 𝑅 ) ) ) )
123 6 110 122 mpbir2and ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Cn ( ordTop ‘ 𝑆 ) ) )