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 24120

Description: Lemma for ordthmeo 24121. (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 6824	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌)
4	2, 3	syl 18	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹:𝑋⟶𝑌)
5		fimacnv 6732	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑌) = 𝑋)
6	4, 5	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) = 𝑋)
7		ordthmeo.1	. . . . . . . . 9 ⊢ 𝑋 = dom 𝑅
8	7	ordttopon 23511	. . . . . . . 8 ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
9	8	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
10		toponmax 23244	. . . . . . 7 ⊢ ((ordTop‘𝑅) ∈ (TopOn‘𝑋) → 𝑋 ∈ (ordTop‘𝑅))
11	9, 10	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑋 ∈ (ordTop‘𝑅))
12	6, 11	eqeltrd 2861	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅))
13		elsni 4601	. . . . . . 7 ⊢ (𝑧 ∈ {𝑌} → 𝑧 = 𝑌)
14	13	imaeq2d 6052	. . . . . 6 ⊢ (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ 𝑌))
15	14	eleq1d 2846	. . . . 5 ⊢ (𝑧 ∈ {𝑌} → ((^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (^◡𝐹 “ 𝑌) ∈ (ordTop‘𝑅)))
16	12, 15	syl5ibrcom 250	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (𝑧 ∈ {𝑌} → (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
17	16	ralrimiv 3154	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
18		cnvimass 6198	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ dom 𝐹
19		f1odm 6828	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → dom 𝐹 = 𝑋)
20	2, 19	syl 18	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → dom 𝐹 = 𝑋)
21	20	adantr 486	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → dom 𝐹 = 𝑋)
22	18, 21	sseqtrid 3973	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋)
23		sseqin2 4169	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
24	22, 23	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
25	2	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋–1-1-onto→𝑌)
26		f1ofn 6825	. . . . . . . . . . . 12 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋)
27	25, 26	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Fn 𝑋)
28		elpreima 7057	. . . . . . . . . . 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 5106	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑦𝑆𝑥 ↔ (𝐹‘𝑧)𝑆𝑥))
35	34	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑦𝑆𝑥 ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
36	35	elrab3 3646	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑧) ∈ 𝑌 → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
37	33, 36	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ↔ ¬ (𝐹‘𝑧)𝑆𝑥))
38		simpll3 1233	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌))
39		f1ocnv 6837	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ^◡𝐹:𝑌–1-1-onto→𝑋)
40		f1of 6824	. . . . . . . . . . . . . . . . 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 5115	. . . . . . . . . . . . 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 4171	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
55	24, 54	eqtr3d 2798	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)})
56		simpl1 1210	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ 𝑉)
57	7	ordtopn1 23512	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
58	56, 42, 57	syl2anc 596	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ 𝑧𝑅(^◡𝐹‘𝑥)} ∈ (ordTop‘𝑅))
59	55, 58	eqeltrd 2861	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
60	59	ralrimiva 3155	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∈ (ordTop‘𝑅))
61		ordthmeo.2	. . . . . . . . . 10 ⊢ 𝑌 = dom 𝑆
62		dmexg 7913	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑊 → dom 𝑆 ∈ V)
63	61, 62	eqeltrid 2865	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑊 → 𝑌 ∈ V)
64	63	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝑌 ∈ V)
65		rabexg 5299	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
66	64, 65	syl 18	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
67	66	ralrimivw 3159	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} ∈ V)
68		eqid 2761	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
69		imaeq2 6048	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}))
70	69	eleq1d 2846	. . . . . . 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 6198	. . . . . . . . . 10 ⊢ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ dom 𝐹
75	74, 21	sseqtrid 3973	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋)
76		sseqin2 4169	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ⊆ 𝑋 ↔ (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
77	75, 76	sylib 221	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
78		elpreima 7057	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
79	27, 78	syl 18	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
80	30	biantrurd 542	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))
81		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝐹‘𝑧) → (𝑥𝑆𝑦 ↔ 𝑥𝑆(𝐹‘𝑧)))
82	81	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹‘𝑧) → (¬ 𝑥𝑆𝑦 ↔ ¬ 𝑥𝑆(𝐹‘𝑧)))
83	82	elrab3 3646	. . . . . . . . . . . 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 5113	. . . . . . . . . . . . 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 4171	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (𝑋 ∩ (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
93	77, 92	eqtr3d 2798	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧})
94	7	ordtopn2 23513	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ (^◡𝐹‘𝑥) ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
95	56, 42, 94	syl2anc 596	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → {𝑧 ∈ 𝑋 ∣ ¬ (^◡𝐹‘𝑥)𝑅𝑧} ∈ (ordTop‘𝑅))
96	93, 95	eqeltrd 2861	. . . . . 6 ⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) ∧ 𝑥 ∈ 𝑌) → (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
97	96	ralrimiva 3155	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) ∈ (ordTop‘𝑅))
98		rabexg 5299	. . . . . . . 8 ⊢ (𝑌 ∈ V → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
99	64, 98	syl 18	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
100	99	ralrimivw 3159	. . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑥 ∈ 𝑌 {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} ∈ V)
101		eqid 2761	. . . . . . 7 ⊢ (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
102		imaeq2 6048	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦} → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))
103	102	eleq1d 2846	. . . . . . 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 4143	. . . 4 ⊢ (∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
108	73, 106, 107	sylanbrc 595	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
109		ralunb 4143	. . 3 ⊢ (∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ↔ (∀𝑧 ∈ {𝑌} (^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅) ∧ ∀𝑧 ∈ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅)))
110	17, 108, 109	sylanbrc 595	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → ∀𝑧 ∈ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})))(^◡𝐹 “ 𝑧) ∈ (ordTop‘𝑅))
111		eqid 2761	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥})
112		eqid 2761	. . . . . . 7 ⊢ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}) = ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦})
113	61, 111, 112	ordtuni 23508	. . . . . 6 ⊢ (𝑆 ∈ 𝑊 → 𝑌 = ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))
114	113, 63	eqeltrrd 2862	. . . . 5 ⊢ (𝑆 ∈ 𝑊 → ∪ ({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))) ∈ V)
115		uniexb 7778	. . . . 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 23507	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
119	118	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) = (topGen‘(fi‘({𝑌} ∪ (ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑦𝑆𝑥}) ∪ ran (𝑥 ∈ 𝑌 ↦ {𝑦 ∈ 𝑌 ∣ ¬ 𝑥𝑆𝑦}))))))
120	61	ordttopon 23511	. . . 4 ⊢ (𝑆 ∈ 𝑊 → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
121	120	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → (ordTop‘𝑆) ∈ (TopOn‘𝑌))
122	9, 117, 119, 121	subbascn 23572	. 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 2145 ∀wral 3077 {crab 3413 Vcvv 3451 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 {csn 4584 ∪ cuni 4867 class class class wbr 5103 ↦ cmpt 5186 ^◡ccnv 5650 dom cdm 5651 ran crn 5652 “ cima 5654 Fn wfn 6533 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 Isom wiso 6539 (class class class)co 7420 ficfi 9402 topGenctg 17608 ordTopcordt 17671 TopOnctopon 23228 Cn ccn 23542

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-1o 8476 df-2o 8477 df-map 8849 df-en 8974 df-dom 8975 df-fin 8977 df-fi 9403 df-topgen 17614 df-ordt 17673 df-top 23212 df-topon 23229 df-bases 23264 df-cn 23545

This theorem is used by: ordthmeo 24121 xrmulc1cn 34562

W3C validator