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 22406

Description: Lemma for ordthmeo 22407. (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 7055	. . . 4 ⊢ (𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
2	1	3ad2ant3 1132	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌)
3		f1of 6590	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌)
4	2, 3	syl 17	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋⟶𝑌)
5		fimacnv 6816	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑌) = 𝑋)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) = 𝑋)
7		ordthmeo.1	. . . . . . . . 9 ⊢ 𝑋 = dom 𝑅
8	7	ordttopon 21798	. . . . . . . 8 ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
9	8	3ad2ant1 1130	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
10		toponmax 21531	. . . . . . 7 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘𝑋) → 𝑋 ∈ (ordTop‘𝑅))
11	9, 10	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑋 ∈ (ordTop‘𝑅))
12	6, 11	eqeltrd 2890	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅))
13		elsni 4542	. . . . . . 7 ⊢ (𝑧 ∈ {𝑌} → 𝑧 = 𝑌)
14	13	imaeq2d 5896	. . . . . 6 ⊢ (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ 𝑌))
15	14	eleq1d 2874	. . . . 5 ⊢ (𝑧 ∈ {𝑌} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅)))
16	12, 15	syl5ibrcom 250	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
17	16	ralrimiv 3148	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
18		cnvimass 5916	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ dom 𝐹
19		f1odm 6594	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → dom 𝐹 = 𝑋)
20	2, 19	syl 17	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → dom 𝐹 = 𝑋)
21	20	adantr 484	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → dom 𝐹 = 𝑋)
22	18, 21	sseqtrid 3967	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋)
23		sseqin2 4142	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
24	22, 23	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
25	2	ad2antrr 725	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋–1-1-onto→𝑌)
26		f1ofn 6591	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋)
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Fn 𝑋)
28		elpreima 6805	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
29	27, 28	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
30		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
31	30	biantrurd 536	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
32	4	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋⟶𝑌)
33	32	ffvelrnda 6828	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ 𝑌)
34		breq1 5033	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑦𝑆𝑥 ↔ (𝐹‘𝑧)𝑆𝑥))
35	34	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑦𝑆𝑥 ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
36	35	elrab3 3629	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
37	33, 36	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
38		simpll3 1211	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌))
39		f1ocnv 6602	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6590	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
41	2, 39, 40	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ^◡𝐹:𝑌⟶𝑋)
42	41	ffvelrnda 6828	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
43	42	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (^◡𝐹‘𝑥) ∈ 𝑋)
44		isorel 7058	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ (^◡𝐹‘𝑥) ∈ 𝑋)) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
45	38, 30, 43, 44	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
46		f1ocnvfv2 7012	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
47	2, 46	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
48	47	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
49	48	breq2d 5042	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥)) ↔ (𝐹‘𝑧)𝑆𝑥))
50	45, 49	bitrd 282	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆𝑥))
51	50	notbid 321	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ 𝑧𝑅(^◡𝐹‘𝑥) ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
52	37, 51	bitr4d 285	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ 𝑧𝑅(^◡𝐹‘𝑥)))
53	29, 31, 52	3bitr2d 310	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ ¬ 𝑧𝑅(^◡𝐹‘𝑥)))
54	53	rabbi2dva 4144	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
55	24, 54	eqtr3d 2835	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
56		simpl1 1188	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ 𝑉)
57	7	ordtopn1 21799	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
58	56, 42, 57	syl2anc 587	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
59	55, 58	eqeltrd 2890	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
60	59	ralrimiva 3149	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
61		ordthmeo.2	. . . . . . . . . 10 ⊢ 𝑌 = dom 𝑆
62		dmexg 7594	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑊 → dom 𝑆 ∈ V)
63	61, 62	eqeltrid 2894	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑊 → 𝑌 ∈ V)
64	63	3ad2ant2 1131	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑌 ∈ V)
65		rabexg 5198	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
66	64, 65	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
67	66	ralrimivw 3150	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
68		eqid 2798	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
69		imaeq2 5892	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
70	69	eleq1d 2874	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
71	68, 70	ralrnmptw 6837	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
72	67, 71	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
73	60, 72	mpbird 260	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
74		cnvimass 5916	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ dom 𝐹
75	74, 21	sseqtrid 3967	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋)
76		sseqin2 4142	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
77	75, 76	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
78		elpreima 6805	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
79	27, 78	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
80	30	biantrurd 536	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
81		breq2 5034	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑥𝑆𝑦 ↔ 𝑥𝑆(𝐹‘𝑧)))
82	81	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑥𝑆𝑦 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
83	82	elrab3 3629	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
84	33, 83	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
85		isorel 7058	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ ((^◡𝐹‘𝑥) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
86	38, 43, 30, 85	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
87	48	breq1d 5040	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧) ↔ 𝑥𝑆(𝐹‘𝑧)))
88	86, 87	bitrd 282	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ 𝑥𝑆(𝐹‘𝑧)))
89	88	notbid 321	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (¬ (^◡𝐹‘𝑥)𝑅𝑧 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
90	84, 89	bitr4d 285	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ (^◡𝐹‘𝑥)𝑅𝑧))
91	79, 80, 90	3bitr2d 310	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ ¬ (^◡𝐹‘𝑥)𝑅𝑧))
92	91	rabbi2dva 4144	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
93	77, 92	eqtr3d 2835	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
94	7	ordtopn2 21800	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
95	56, 42, 94	syl2anc 587	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
96	93, 95	eqeltrd 2890	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
97	96	ralrimiva 3149	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
98		rabexg 5198	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
99	64, 98	syl 17	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
100	99	ralrimivw 3150	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
101		eqid 2798	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
102		imaeq2 5892	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
103	102	eleq1d 2874	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
104	101, 103	ralrnmptw 6837	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
105	100, 104	syl 17	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
106	97, 105	mpbird 260	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
107		ralunb 4118	. . . 4 ⊢ (∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
108	73, 106, 107	sylanbrc 586	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
109		ralunb 4118	. . 3 ⊢ (∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
110	17, 108, 109	sylanbrc 586	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
111		eqid 2798	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
112		eqid 2798	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
113	61, 111, 112	ordtuni 21795	. . . . . 6 ⊢ (𝑆 ∈ 𝑊 → 𝑌 = ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))
114	113, 63	eqeltrrd 2891	. . . . 5 ⊢ (𝑆 ∈ 𝑊 → ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
115		uniexb 7466	. . . . 5 ⊢ (({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V ↔ ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
116	114, 115	sylibr 237	. . . 4 ⊢ (𝑆 ∈ 𝑊 → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
117	116	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
118	61, 111, 112	ordtval 21794	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
119	118	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
120	61	ordttopon 21798	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
121	120	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
122	9, 117, 119, 121	subbascn 21859	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))))
123	4, 110, 122	mpbir2and 712	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 {crab 3110 Vcvv 3441 ∪ cun 3879 ∩ cin 3880 ⊆ wss 3881 {csn 4525 ∪ cuni 4800 class class class wbr 5030 ↦ cmpt 5110 ^◡ccnv 5518 dom cdm 5519 ran crn 5520 “ cima 5522 Fn wfn 6319 ⟶wf 6320 –1-1-onto→wf1o 6323 ‘cfv 6324 Isom wiso 6325 (class class class)co 7135 ficfi 8858 topGenctg 16703 ordTopcordt 16764 TopOnctopon 21515 Cn ccn 21829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-fin 8496 df-fi 8859 df-topgen 16709 df-ordt 16766 df-top 21499 df-topon 21516 df-bases 21551 df-cn 21832

This theorem is referenced by: ordthmeo 22407 xrmulc1cn 31283

W3C validator