| 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 ‘ 𝑆 ) ) ) |