ordthmeolem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ordthmeolem		Structured version Visualization version GIF version

Theorem ordthmeolem 23739

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

**Hypotheses**
Ref	Expression
ordthmeo.1	⊢ 𝑋 = dom 𝑅
ordthmeo.2	⊢ 𝑌 = dom 𝑆

**Assertion**
Ref	Expression
ordthmeolem	⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))

Proof of Theorem ordthmeolem Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isof1o 7316	. . . 4 ⊢ (𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
2	1	3ad2ant3 1135	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌)
3		f1of 6818	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌)
4	2, 3	syl 17	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋⟶𝑌)
5		fimacnv 6728	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑌) = 𝑋)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) = 𝑋)
7		ordthmeo.1	. . . . . . . . 9 ⊢ 𝑋 = dom 𝑅
8	7	ordttopon 23131	. . . . . . . 8 ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
9	8	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
10		toponmax 22864	. . . . . . 7 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘𝑋) → 𝑋 ∈ (ordTop‘𝑅))
11	9, 10	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑋 ∈ (ordTop‘𝑅))
12	6, 11	eqeltrd 2834	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅))
13		elsni 4618	. . . . . . 7 ⊢ (𝑧 ∈ {𝑌} → 𝑧 = 𝑌)
14	13	imaeq2d 6047	. . . . . 6 ⊢ (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ 𝑌))
15	14	eleq1d 2819	. . . . 5 ⊢ (𝑧 ∈ {𝑌} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅)))
16	12, 15	syl5ibrcom 247	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
17	16	ralrimiv 3131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
18		cnvimass 6069	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ dom 𝐹
19		f1odm 6822	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → dom 𝐹 = 𝑋)
20	2, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → dom 𝐹 = 𝑋)
21	20	adantr 480	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → dom 𝐹 = 𝑋)
22	18, 21	sseqtrid 4001	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋)
23		sseqin2 4198	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
24	22, 23	sylib 218	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
25	2	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋–1-1-onto→𝑌)
26		f1ofn 6819	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋)
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Fn 𝑋)
28		elpreima 7048	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
29	27, 28	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
30		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
31	30	biantrurd 532	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
32	4	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋⟶𝑌)
33	32	ffvelcdmda 7074	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ 𝑌)
34		breq1 5122	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑦𝑆𝑥 ↔ (𝐹‘𝑧)𝑆𝑥))
35	34	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑦𝑆𝑥 ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
36	35	elrab3 3672	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
37	33, 36	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
38		simpll3 1215	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌))
39		f1ocnv 6830	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6818	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
41	2, 39, 40	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ^◡𝐹:𝑌⟶𝑋)
42	41	ffvelcdmda 7074	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
43	42	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (^◡𝐹‘𝑥) ∈ 𝑋)
44		isorel 7319	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ (^◡𝐹‘𝑥) ∈ 𝑋)) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
45	38, 30, 43, 44	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
46		f1ocnvfv2 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
47	2, 46	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
48	47	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
49	48	breq2d 5131	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥)) ↔ (𝐹‘𝑧)𝑆𝑥))
50	45, 49	bitrd 279	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆𝑥))
51	50	notbid 318	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ 𝑧𝑅(^◡𝐹‘𝑥) ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
52	37, 51	bitr4d 282	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ 𝑧𝑅(^◡𝐹‘𝑥)))
53	29, 31, 52	3bitr2d 307	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ ¬ 𝑧𝑅(^◡𝐹‘𝑥)))
54	53	rabbi2dva 4201	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
55	24, 54	eqtr3d 2772	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
56		simpl1 1192	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ 𝑉)
57	7	ordtopn1 23132	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
58	56, 42, 57	syl2anc 584	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
59	55, 58	eqeltrd 2834	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
60	59	ralrimiva 3132	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
61		ordthmeo.2	. . . . . . . . . 10 ⊢ 𝑌 = dom 𝑆
62		dmexg 7897	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑊 → dom 𝑆 ∈ V)
63	61, 62	eqeltrid 2838	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑊 → 𝑌 ∈ V)
64	63	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑌 ∈ V)
65		rabexg 5307	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
66	64, 65	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
67	66	ralrimivw 3136	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
68		eqid 2735	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
69		imaeq2 6043	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
70	69	eleq1d 2819	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
71	68, 70	ralrnmptw 7084	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
72	67, 71	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
73	60, 72	mpbird 257	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
74		cnvimass 6069	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ dom 𝐹
75	74, 21	sseqtrid 4001	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋)
76		sseqin2 4198	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
77	75, 76	sylib 218	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
78		elpreima 7048	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
79	27, 78	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
80	30	biantrurd 532	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
81		breq2 5123	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑥𝑆𝑦 ↔ 𝑥𝑆(𝐹‘𝑧)))
82	81	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑥𝑆𝑦 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
83	82	elrab3 3672	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
84	33, 83	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
85		isorel 7319	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ ((^◡𝐹‘𝑥) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
86	38, 43, 30, 85	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
87	48	breq1d 5129	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧) ↔ 𝑥𝑆(𝐹‘𝑧)))
88	86, 87	bitrd 279	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ 𝑥𝑆(𝐹‘𝑧)))
89	88	notbid 318	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ (^◡𝐹‘𝑥)𝑅𝑧 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
90	84, 89	bitr4d 282	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ (^◡𝐹‘𝑥)𝑅𝑧))
91	79, 80, 90	3bitr2d 307	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ ¬ (^◡𝐹‘𝑥)𝑅𝑧))
92	91	rabbi2dva 4201	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
93	77, 92	eqtr3d 2772	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
94	7	ordtopn2 23133	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
95	56, 42, 94	syl2anc 584	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
96	93, 95	eqeltrd 2834	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
97	96	ralrimiva 3132	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
98		rabexg 5307	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
99	64, 98	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
100	99	ralrimivw 3136	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
101		eqid 2735	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
102		imaeq2 6043	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
103	102	eleq1d 2819	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
104	101, 103	ralrnmptw 7084	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
105	100, 104	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
106	97, 105	mpbird 257	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
107		ralunb 4172	. . . 4 ⊢ (∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
108	73, 106, 107	sylanbrc 583	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
109		ralunb 4172	. . 3 ⊢ (∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
110	17, 108, 109	sylanbrc 583	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
111		eqid 2735	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
112		eqid 2735	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
113	61, 111, 112	ordtuni 23128	. . . . . 6 ⊢ (𝑆 ∈ 𝑊 → 𝑌 = ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))
114	113, 63	eqeltrrd 2835	. . . . 5 ⊢ (𝑆 ∈ 𝑊 → ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
115		uniexb 7758	. . . . 5 ⊢ (({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V ↔ ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
116	114, 115	sylibr 234	. . . 4 ⊢ (𝑆 ∈ 𝑊 → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
117	116	3ad2ant2 1134	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
118	61, 111, 112	ordtval 23127	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
119	118	3ad2ant2 1134	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
120	61	ordttopon 23131	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
121	120	3ad2ant2 1134	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
122	9, 117, 119, 121	subbascn 23192	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))))
123	4, 110, 122	mpbir2and 713	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 {crab 3415 Vcvv 3459 ∪ cun 3924 ∩ cin 3925 ⊆ wss 3926 {csn 4601 ∪ cuni 4883 class class class wbr 5119 ↦ cmpt 5201 ^◡ccnv 5653 dom cdm 5654 ran crn 5655 “ cima 5657 Fn wfn 6526 ⟶wf 6527 –1-1-onto→wf1o 6530 ‘cfv 6531 Isom wiso 6532 (class class class)co 7405 ficfi 9422 topGenctg 17451 ordTopcordt 17513 TopOnctopon 22848 Cn ccn 23162

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-1o 8480 df-2o 8481 df-map 8842 df-en 8960 df-dom 8961 df-fin 8963 df-fi 9423 df-topgen 17457 df-ordt 17515 df-top 22832 df-topon 22849 df-bases 22884 df-cn 23165

This theorem is referenced by: ordthmeo 23740 xrmulc1cn 33961

W3C validator