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 24014

Description: Lemma for ordthmeo 24015. (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 7331	. . . 4 ⊢ (𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) → 𝐹:𝑋–1-1-onto→𝑌)
2	1	3ad2ant3 1153	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌)
3		f1of 6825	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌)
4	2, 3	syl 18	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋⟶𝑌)
5		fimacnv 6733	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑌) = 𝑋)
6	4, 5	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) = 𝑋)
7		ordthmeo.1	. . . . . . . . 9 ⊢ 𝑋 = dom 𝑅
8	7	ordttopon 23405	. . . . . . . 8 ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
9	8	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
10		toponmax 23138	. . . . . . 7 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘𝑋) → 𝑋 ∈ (ordTop‘𝑅))
11	9, 10	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑋 ∈ (ordTop‘𝑅))
12	6, 11	eqeltrd 2865	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅))
13		elsni 4608	. . . . . . 7 ⊢ (𝑧 ∈ {𝑌} → 𝑧 = 𝑌)
14	13	imaeq2d 6064	. . . . . 6 ⊢ (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ 𝑌))
15	14	eleq1d 2850	. . . . 5 ⊢ (𝑧 ∈ {𝑌} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅)))
16	12, 15	syl5ibrcom 250	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
17	16	ralrimiv 3158	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
18		cnvimass 6086	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ dom 𝐹
19		f1odm 6829	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → dom 𝐹 = 𝑋)
20	2, 19	syl 18	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → dom 𝐹 = 𝑋)
21	20	adantr 486	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → dom 𝐹 = 𝑋)
22	18, 21	sseqtrid 3980	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋)
23		sseqin2 4176	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
24	22, 23	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
25	2	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋–1-1-onto→𝑌)
26		f1ofn 6826	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋)
27	25, 26	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Fn 𝑋)
28		elpreima 7058	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
29	27, 28	syl 18	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
30		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
31	30	biantrurd 542	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})))
32	4	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝐹:𝑋⟶𝑌)
33	32	ffvelcdmda 7084	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ 𝑌)
34		breq1 5114	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑦𝑆𝑥 ↔ (𝐹‘𝑧)𝑆𝑥))
35	34	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑦𝑆𝑥 ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
36	35	elrab3 3653	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
37	33, 36	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
38		simpll3 1233	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌))
39		f1ocnv 6838	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6825	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑌–1-1-onto→𝑋 → ^◡𝐹:𝑌⟶𝑋)
41	2, 39, 40	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ^◡𝐹:𝑌⟶𝑋)
42	41	ffvelcdmda 7084	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹‘𝑥) ∈ 𝑋)
43	42	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (^◡𝐹‘𝑥) ∈ 𝑋)
44		isorel 7334	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ (^◡𝐹‘𝑥) ∈ 𝑋)) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
45	38, 30, 43, 44	syl12anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧𝑅(^◡𝐹‘𝑥) ↔ (𝐹‘𝑧)𝑆(𝐹‘(^◡𝐹‘𝑥))))
46		f1ocnvfv2 7285	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
47	2, 46	sylan 592	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
48	47	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
49	48	breq2d 5123	. . . . . . . . . . . . 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 4178	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
55	24, 54	eqtr3d 2802	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
56		simpl1 1210	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ 𝑉)
57	7	ordtopn1 23406	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
58	56, 42, 57	syl2anc 596	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
59	55, 58	eqeltrd 2865	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
60	59	ralrimiva 3159	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
61		ordthmeo.2	. . . . . . . . . 10 ⊢ 𝑌 = dom 𝑆
62		dmexg 7905	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑊 → dom 𝑆 ∈ V)
63	61, 62	eqeltrid 2869	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑊 → 𝑌 ∈ V)
64	63	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑌 ∈ V)
65		rabexg 5310	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
66	64, 65	syl 18	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
67	66	ralrimivw 3163	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
68		eqid 2765	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
69		imaeq2 6060	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
70	69	eleq1d 2850	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
71	68, 70	ralrnmptw 7094	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
72	67, 71	syl 18	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅)))
73	60, 72	mpbird 260	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
74		cnvimass 6086	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ dom 𝐹
75	74, 21	sseqtrid 3980	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋)
76		sseqin2 4176	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
77	75, 76	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
78		elpreima 7058	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
79	27, 78	syl 18	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
80	30	biantrurd 542	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
81		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑥𝑆𝑦 ↔ 𝑥𝑆(𝐹‘𝑧)))
82	81	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑥𝑆𝑦 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
83	82	elrab3 3653	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
84	33, 83	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
85		isorel 7334	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌) ∧ ((^◡𝐹‘𝑥) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
86	38, 43, 30, 85	syl12anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((^◡𝐹‘𝑥)𝑅𝑧 ↔ (𝐹‘(^◡𝐹‘𝑥))𝑆(𝐹‘𝑧)))
87	48	breq1d 5121	. . . . . . . . . . . . 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 4178	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
93	77, 92	eqtr3d 2802	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
94	7	ordtopn2 23407	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
95	56, 42, 94	syl2anc 596	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
96	93, 95	eqeltrd 2865	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
97	96	ralrimiva 3159	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
98		rabexg 5310	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
99	64, 98	syl 18	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
100	99	ralrimivw 3163	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
101		eqid 2765	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
102		imaeq2 6060	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
103	102	eleq1d 2850	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
104	101, 103	ralrnmptw 7094	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
105	100, 104	syl 18	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅)))
106	97, 105	mpbird 260	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
107		ralunb 4150	. . . 4 ⊢ (∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
108	73, 106, 107	sylanbrc 595	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
109		ralunb 4150	. . 3 ⊢ (∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
110	17, 108, 109	sylanbrc 595	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
111		eqid 2765	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
112		eqid 2765	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
113	61, 111, 112	ordtuni 23402	. . . . . 6 ⊢ (𝑆 ∈ 𝑊 → 𝑌 = ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))
114	113, 63	eqeltrrd 2866	. . . . 5 ⊢ (𝑆 ∈ 𝑊 → ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
115		uniexb 7770	. . . . 5 ⊢ (({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V ↔ ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
116	114, 115	sylibr 237	. . . 4 ⊢ (𝑆 ∈ 𝑊 → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
117	116	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
118	61, 111, 112	ordtval 23401	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
119	118	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
120	61	ordttopon 23405	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
121	120	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
122	9, 117, 119, 121	subbascn 23466	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))))
123	4, 110, 122	mpbir2and 726	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∀wral 3081 {crab 3418 Vcvv 3457 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 {csn 4591 ∪ cuni 4874 class class class wbr 5111 ↦ cmpt 5194 ^◡ccnv 5662 dom cdm 5663 ran crn 5664 “ cima 5666 Fn wfn 6536 ⟶wf 6537 –1-1-onto→wf1o 6540 ‘cfv 6541 Isom wiso 6542 (class class class)co 7420 ficfi 9378 topGenctg 17517 ordTopcordt 17580 TopOnctopon 23122 Cn ccn 23436

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7743

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7870 df-1st 7993 df-2nd 7994 df-1o 8460 df-2o 8461 df-map 8833 df-en 8951 df-dom 8952 df-fin 8954 df-fi 9379 df-topgen 17523 df-ordt 17582 df-top 23106 df-topon 23123 df-bases 23158 df-cn 23439

This theorem is used by: ordthmeo 24015 xrmulc1cn 34389

W3C validator