Theorem ordthmeolem 23725

Description: Lemma for ordthmeo 23726. (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 7337	. . . 4 ⊢ (𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
2	1	3ad2ant3 1132	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌)
3		f1of 6844	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌)
4	2, 3	syl 17	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋⟶𝑌)
5		fimacnv 6750	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (◡𝐹 “ 𝑌) = 𝑋)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (◡𝐹 “ 𝑌) = 𝑋)
7		ordthmeo.1	. . . . . . . . 9 ⊢ 𝑋 = dom 𝑅
8	7	ordttopon 23117	. . . . . . . 8 ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
9	8	3ad2ant1 1130	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
10		toponmax 22848	. . . . . . 7 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘𝑋) → 𝑋 ∈ (ordTop‘𝑅))
11	9, 10	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑋 ∈ (ordTop‘𝑅))
12	6, 11	eqeltrd 2829	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅))
13		elsni 4649	. . . . . . 7 ⊢ (𝑧 ∈ {𝑌} → 𝑧 = 𝑌)
14	13	imaeq2d 6068	. . . . . 6 ⊢ (𝑧 ∈ {𝑌} → (◡𝐹 “ 𝑧) = (◡𝐹 “ 𝑌))
15	14	eleq1d 2814	. . . . 5 ⊢ (𝑧 ∈ {𝑌} → ((◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅)))
16	12, 15	syl5ibrcom 246	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝑧 ∈ {𝑌} → (◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
17	16	ralrimiv 3142	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ {𝑌} (◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
18		cnvimass 6090	. . . . . . . . . 10 ⊢ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ dom 𝐹
19		f1odm 6848	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → dom 𝐹 = 𝑋)
20	2, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → dom 𝐹 = 𝑋)
21	20	adantr 479	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → dom 𝐹 = 𝑋)
22	18, 21	sseqtrid 4034	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋)
23		sseqin2 4217	. . . . . . . . 9 ⊢ ((◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋 ↔ (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
24	22, 23	sylib 217	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
25	2	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋–1-1-onto→𝑌)
26		f1ofn 6845	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋)
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Fn 𝑋)
28		elpreima 7072	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
29	27, 28	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
30		simpr 483	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
31	30	biantrurd 531	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
32	4	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋⟶𝑌)
33	32	ffvelcdmda 7099	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ 𝑌)
34		breq1 5155	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑦𝑆𝑥 ↔ (𝐹‘𝑧)𝑆𝑥))
35	34	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑦𝑆𝑥 ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
36	35	elrab3 3685	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
37	33, 36	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
38		simpll3 1211	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌))
39		f1ocnv 6856	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6844	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋)
41	2, 39, 40	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ◡𝐹:𝑌⟶𝑋)
42	41	ffvelcdmda 7099	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹‘𝑥) ∈ 𝑋)
43	42	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (◡𝐹‘𝑥) ∈ 𝑋)
44		isorel 7340	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ (◡𝐹‘𝑥) ∈ 𝑋)) → (𝑧𝑅(◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(◡𝐹‘𝑥))))
45	38, 30, 43, 44	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(◡𝐹‘𝑥))))
46		f1ocnvfv2 7292	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥)
47	2, 46	sylan 578	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥)
48	47	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥)
49	48	breq2d 5164	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧)𝑆(𝐹‘(◡𝐹‘𝑥)) ↔ (𝐹‘𝑧)𝑆𝑥))
50	45, 49	bitrd 278	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆𝑥))
51	50	notbid 317	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ 𝑧𝑅(◡𝐹‘𝑥) ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
52	37, 51	bitr4d 281	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ 𝑧𝑅(◡𝐹‘𝑥)))
53	29, 31, 52	3bitr2d 306	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ ¬ 𝑧𝑅(◡𝐹‘𝑥)))
54	53	rabbi2dva 4220	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(◡𝐹‘𝑥)})
55	24, 54	eqtr3d 2770	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(◡𝐹‘𝑥)})
56		simpl1 1188	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ 𝑉)
57	7	ordtopn1 23118	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
58	56, 42, 57	syl2anc 582	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
59	55, 58	eqeltrd 2829	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
60	59	ralrimiva 3143	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
61		ordthmeo.2	. . . . . . . . . 10 ⊢ 𝑌 = dom 𝑆
62		dmexg 7915	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑊 → dom 𝑆 ∈ V)
63	61, 62	eqeltrid 2833	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑊 → 𝑌 ∈ V)
64	63	3ad2ant2 1131	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑌 ∈ V)
65		rabexg 5337	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
66	64, 65	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
67	66	ralrimivw 3147	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
68		eqid 2728	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
69		imaeq2 6064	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → (◡𝐹 “ 𝑧) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
70	69	eleq1d 2814	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → ((◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
71	68, 70	ralrnmptw 7109	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
72	67, 71	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
73	60, 72	mpbird 256	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
74		cnvimass 6090	. . . . . . . . . 10 ⊢ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ dom 𝐹
75	74, 21	sseqtrid 4034	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋)
76		sseqin2 4217	. . . . . . . . 9 ⊢ ((◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋 ↔ (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
77	75, 76	sylib 217	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
78		elpreima 7072	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
79	27, 78	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
80	30	biantrurd 531	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
81		breq2 5156	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑥𝑆𝑦 ↔ 𝑥𝑆(𝐹‘𝑧)))
82	81	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑥𝑆𝑦 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
83	82	elrab3 3685	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
84	33, 83	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
85		isorel 7340	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ ((◡𝐹‘𝑥) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
86	38, 43, 30, 85	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
87	48	breq1d 5162	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘(◡𝐹‘𝑥))𝑆(𝐹‘𝑧) ↔ 𝑥𝑆(𝐹‘𝑧)))
88	86, 87	bitrd 278	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((◡𝐹‘𝑥)𝑅𝑧 ↔ 𝑥𝑆(𝐹‘𝑧)))
89	88	notbid 317	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ (◡𝐹‘𝑥)𝑅𝑧 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
90	84, 89	bitr4d 281	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ (◡𝐹‘𝑥)𝑅𝑧))
91	79, 80, 90	3bitr2d 306	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ ¬ (◡𝐹‘𝑥)𝑅𝑧))
92	91	rabbi2dva 4220	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = {𝑧 ∈ 𝑋 ∣ ¬ (◡𝐹‘𝑥)𝑅𝑧})
93	77, 92	eqtr3d 2770	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = {𝑧 ∈ 𝑋 ∣ ¬ (◡𝐹‘𝑥)𝑅𝑧})
94	7	ordtopn2 23119	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ (◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
95	56, 42, 94	syl2anc 582	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ (◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
96	93, 95	eqeltrd 2829	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
97	96	ralrimiva 3143	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
98		rabexg 5337	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
99	64, 98	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
100	99	ralrimivw 3147	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
101		eqid 2728	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
102		imaeq2 6064	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → (◡𝐹 “ 𝑧) = (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
103	102	eleq1d 2814	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → ((◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
104	101, 103	ralrnmptw 7109	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
105	100, 104	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
106	97, 105	mpbird 256	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
107		ralunb 4193	. . . 4 ⊢ (∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
108	73, 106, 107	sylanbrc 581	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
109		ralunb 4193	. . 3 ⊢ (∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ {𝑌} (◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
110	17, 108, 109	sylanbrc 581	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
111		eqid 2728	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
112		eqid 2728	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
113	61, 111, 112	ordtuni 23114	. . . . . 6 ⊢ (𝑆 ∈ 𝑊 → 𝑌 = ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))
114	113, 63	eqeltrrd 2830	. . . . 5 ⊢ (𝑆 ∈ 𝑊 → ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
115		uniexb 7772	. . . . 5 ⊢ (({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V ↔ ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
116	114, 115	sylibr 233	. . . 4 ⊢ (𝑆 ∈ 𝑊 → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
117	116	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
118	61, 111, 112	ordtval 23113	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
119	118	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
120	61	ordttopon 23117	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
121	120	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
122	9, 117, 119, 121	subbascn 23178	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))))
123	4, 110, 122	mpbir2and 711	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∀wral 3058  {crab 3430  Vcvv 3473   ∪ cun 3947   ∩ cin 3948   ⊆ wss 3949  {csn 4632  ∪ cuni 4912   class class class wbr 5152   ↦ cmpt 5235  ^◡ccnv 5681  dom cdm 5682  ran crn 5683   “ cima 5685   Fn wfn 6548  ⟶wf 6549  –1-1-onto→wf1o 6552  ‘cfv 6553   Isom wiso 6554  (class class class)co 7426  ficfi 9441  topGenctg 17426  ordTopcordt 17488  TopOnctopon 22832   Cn ccn 23148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-1o 8493  df-er 8731  df-map 8853  df-en 8971  df-dom 8972  df-fin 8974  df-fi 9442  df-topgen 17432  df-ordt 17490  df-top 22816  df-topon 22833  df-bases 22869  df-cn 23151

This theorem is referenced by:  ordthmeo  23726  xrmulc1cn  33564