Theorem ordtrest2NEW 34083

Description: An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)

Hypotheses

Ref	Expression
ordtNEW.b	⊢ 𝐵 = (Base‘𝐾)
ordtNEW.l	⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtrest2NEW.2	⊢ (𝜑 → 𝐾 ∈ Toset)
ordtrest2NEW.3	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
ordtrest2NEW.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)

Assertion

Ref	Expression
ordtrest2NEW	⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴))

Distinct variable groups:   𝑥,𝑦, ≤   𝑥,𝐵,𝑦   𝑥,𝐾,𝑦   𝑥,𝐴,𝑦,𝑧   𝑧, ≤   𝑧,𝐴   𝑧,𝐵   𝜑,𝑥,𝑦,𝑧   𝑧,𝐾

Proof of Theorem ordtrest2NEW

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordtrest2NEW.2	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Toset)
2		tospos 18375	. . . 4 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
3		posprs 18273	. . . 4 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
4	1, 2, 3	3syl 18	. . 3 ⊢ (𝜑 → 𝐾 ∈ Proset )
5		ordtrest2NEW.3	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
6		ordtNEW.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
7		ordtNEW.l	. . . 4 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
8	6, 7	ordtrestNEW 34081	. . 3 ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴))
9	4, 5, 8	syl2anc 585	. 2 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴))
10		eqid 2737	. . . . . . . 8 ⊢ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})
11		eqid 2737	. . . . . . . 8 ⊢ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})
12	6, 7, 10, 11	ordtprsval 34078	. . . . . . 7 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))))
13	4, 12	syl 17	. . . . . 6 ⊢ (𝜑 → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))))
14	13	oveq1d 7375	. . . . 5 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) = ((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴))
15		fibas 22952	. . . . . 6 ⊢ (fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ∈ TopBases
16	6	fvexi 6848	. . . . . . . 8 ⊢ 𝐵 ∈ V
17	16	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
18	17, 5	ssexd 5261	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ V)
19		tgrest 23134	. . . . . 6 ⊢ (((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ∈ TopBases ∧ 𝐴 ∈ V) → (topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴))
20	15, 18, 19	sylancr 588	. . . . 5 ⊢ (𝜑 → (topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴))
21	14, 20	eqtr4d 2775	. . . 4 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) = (topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)))
22		firest 17386	. . . . 5 ⊢ (fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴)) = ((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)
23	22	fveq2i 6837	. . . 4 ⊢ (topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) = (topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴))
24	21, 23	eqtr4di 2790	. . 3 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) = (topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))))
25		fvex 6847	. . . . . . . 8 ⊢ (le‘𝐾) ∈ V
26	25	inex1 5254	. . . . . . 7 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
27	7, 26	eqeltri 2833	. . . . . 6 ⊢ ≤ ∈ V
28	27	inex1 5254	. . . . 5 ⊢ ( ≤ ∩ (𝐴 × 𝐴)) ∈ V
29		ordttop 23175	. . . . 5 ⊢ (( ≤ ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top)
30	28, 29	mp1i 13	. . . 4 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top)
31	6, 7, 10, 11	ordtprsuni 34079	. . . . . . . . 9 ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))
32	4, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = ∪ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))
33	32, 17	eqeltrrd 2838	. . . . . . 7 ⊢ (𝜑 → ∪ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V)
34		uniexb 7711	. . . . . . 7 ⊢ (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V ↔ ∪ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V)
35	33, 34	sylibr 234	. . . . . 6 ⊢ (𝜑 → ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V)
36		restval 17380	. . . . . 6 ⊢ ((({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V ∧ 𝐴 ∈ V) → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)))
37	35, 18, 36	syl2anc 585	. . . . 5 ⊢ (𝜑 → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)))
38		sseqin2 4164	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴)
39	5, 38	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 ∩ 𝐴) = 𝐴)
40		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ dom ( ≤ ∩ (𝐴 × 𝐴)) = dom ( ≤ ∩ (𝐴 × 𝐴))
41	40	ordttopon 23168	. . . . . . . . . . . . . 14 ⊢ (( ≤ ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))))
42	28, 41	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))))
43	6, 7	prsssdm 34077	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
44	4, 5, 43	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
45	44	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (TopOn‘dom ( ≤ ∩ (𝐴 × 𝐴))) = (TopOn‘𝐴))
46	42, 45	eleqtrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴))
47		toponmax 22901	. . . . . . . . . . . 12 ⊢ ((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
49	39, 48	eqeltrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
50		elsni 4585	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ {𝐵} → 𝑣 = 𝐵)
51	50	ineq1d 4160	. . . . . . . . . . 11 ⊢ (𝑣 ∈ {𝐵} → (𝑣 ∩ 𝐴) = (𝐵 ∩ 𝐴))
52	51	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝐵} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝐵 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
53	49, 52	syl5ibrcom 247	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ {𝐵} → (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
54	53	ralrimiv 3129	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ {𝐵} (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
55		ordtrest2NEW.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)
56	6, 7, 1, 5, 55	ordtrest2NEWlem 34082	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
57		eqid 2737	. . . . . . . . . . . 12 ⊢ (ODual‘𝐾) = (ODual‘𝐾)
58	57, 6	odubas 18248	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘(ODual‘𝐾))
59	7	cnveqi 5823	. . . . . . . . . . . 12 ⊢ ◡ ≤ = ◡((le‘𝐾) ∩ (𝐵 × 𝐵))
60		cnvin 6102	. . . . . . . . . . . . 13 ⊢ ◡((le‘𝐾) ∩ (𝐵 × 𝐵)) = (◡(le‘𝐾) ∩ ◡(𝐵 × 𝐵))
61		cnvxp 6115	. . . . . . . . . . . . . 14 ⊢ ◡(𝐵 × 𝐵) = (𝐵 × 𝐵)
62	61	ineq2i 4158	. . . . . . . . . . . . 13 ⊢ (◡(le‘𝐾) ∩ ◡(𝐵 × 𝐵)) = (◡(le‘𝐾) ∩ (𝐵 × 𝐵))
63		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) = (le‘𝐾)
64	57, 63	oduleval 18246	. . . . . . . . . . . . . 14 ⊢ ◡(le‘𝐾) = (le‘(ODual‘𝐾))
65	64	ineq1i 4157	. . . . . . . . . . . . 13 ⊢ (◡(le‘𝐾) ∩ (𝐵 × 𝐵)) = ((le‘(ODual‘𝐾)) ∩ (𝐵 × 𝐵))
66	60, 62, 65	3eqtri 2764	. . . . . . . . . . . 12 ⊢ ◡((le‘𝐾) ∩ (𝐵 × 𝐵)) = ((le‘(ODual‘𝐾)) ∩ (𝐵 × 𝐵))
67	59, 66	eqtri 2760	. . . . . . . . . . 11 ⊢ ◡ ≤ = ((le‘(ODual‘𝐾)) ∩ (𝐵 × 𝐵))
68	57	odutos 33043	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Toset → (ODual‘𝐾) ∈ Toset)
69	1, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ODual‘𝐾) ∈ Toset)
70		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
72	70, 71	brcnv 5831	. . . . . . . . . . . . . . 15 ⊢ (𝑦◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑦)
73		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
74	71, 73	brcnv 5831	. . . . . . . . . . . . . . 15 ⊢ (𝑧◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑧)
75	72, 74	anbi12ci 630	. . . . . . . . . . . . . 14 ⊢ ((𝑦◡ ≤ 𝑧 ∧ 𝑧◡ ≤ 𝑥) ↔ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))
76	75	rabbii 3395	. . . . . . . . . . . . 13 ⊢ {𝑧 ∈ 𝐵 ∣ (𝑦◡ ≤ 𝑧 ∧ 𝑧◡ ≤ 𝑥)} = {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}
77	76, 55	eqsstrid 3961	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑦◡ ≤ 𝑧 ∧ 𝑧◡ ≤ 𝑥)} ⊆ 𝐴)
78	77	ancom2s 651	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑦◡ ≤ 𝑧 ∧ 𝑧◡ ≤ 𝑥)} ⊆ 𝐴)
79	58, 67, 69, 5, 78	ordtrest2NEWlem 34082	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡ ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))))
80		vex 3434	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑤 ∈ V
81	80, 71	brcnv 5831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑤)
82	81	bicomi 224	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ≤ 𝑤 ↔ 𝑤◡ ≤ 𝑧)
83	82	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑧 ≤ 𝑤 ↔ 𝑤◡ ≤ 𝑧))
84	83	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (¬ 𝑧 ≤ 𝑤 ↔ ¬ 𝑤◡ ≤ 𝑧))
85	84	rabbidv 3397	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤} = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡ ≤ 𝑧})
86	85	mpteq2dv 5180	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡ ≤ 𝑧}))
87	86	rneqd 5887	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡ ≤ 𝑧}))
88	6	ressprs 33041	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )
89	4, 5, 88	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾s 𝐴) ∈ Proset )
90		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(𝐾 ↾s 𝐴)) = (Base‘(𝐾 ↾s 𝐴))
91		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))
92	90, 91	ordtcnvNEW 34080	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ↾s 𝐴) ∈ Proset → (ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) = (ordTop‘((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))))
93	89, 92	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) = (ordTop‘((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))))
94	6, 7	prsss 34076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴)))
95	4, 5, 94	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴)))
96		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴)
97	96, 63	ressle 17334	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ V → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴)))
98	18, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴)))
99	96, 6	ressbas2 17199	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝐾 ↾s 𝐴)))
100	5, 99	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 = (Base‘(𝐾 ↾s 𝐴)))
101	100	sqxpeqd 5656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴 × 𝐴) = ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))
102	98, 101	ineq12d 4162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((le‘𝐾) ∩ (𝐴 × 𝐴)) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))
103	95, 102	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))
104	103	cnveqd 5824	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ◡( ≤ ∩ (𝐴 × 𝐴)) = ◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))
105	104	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ordTop‘◡( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))))
106	103	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))))
107	93, 105, 106	3eqtr4d 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ordTop‘◡( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
108		cnvin 6102	. . . . . . . . . . . . . . 15 ⊢ ◡( ≤ ∩ (𝐴 × 𝐴)) = (◡ ≤ ∩ ◡(𝐴 × 𝐴))
109		cnvxp 6115	. . . . . . . . . . . . . . . 16 ⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴)
110	109	ineq2i 4158	. . . . . . . . . . . . . . 15 ⊢ (◡ ≤ ∩ ◡(𝐴 × 𝐴)) = (◡ ≤ ∩ (𝐴 × 𝐴))
111	108, 110	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ ◡( ≤ ∩ (𝐴 × 𝐴)) = (◡ ≤ ∩ (𝐴 × 𝐴))
112	111	fveq2i 6837	. . . . . . . . . . . . 13 ⊢ (ordTop‘◡( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))
113	107, 112	eqtr3di 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))))
114	113	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))))
115	87, 114	raleqbidv 3312	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡ ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))))
116	79, 115	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
117		ralunb 4138	. . . . . . . . 9 ⊢ (∀𝑣 ∈ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
118	56, 116, 117	sylanbrc 584	. . . . . . . 8 ⊢ (𝜑 → ∀𝑣 ∈ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
119		ralunb 4138	. . . . . . . 8 ⊢ (∀𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ {𝐵} (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))))
120	54, 118, 119	sylanbrc 584	. . . . . . 7 ⊢ (𝜑 → ∀𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
121		eqid 2737	. . . . . . . 8 ⊢ (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴))
122	121	fmpt 7056	. . . . . . 7 ⊢ (∀𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))⟶(ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
123	120, 122	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))⟶(ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
124	123	frnd 6670	. . . . 5 ⊢ (𝜑 → ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
125	37, 124	eqsstrd 3957	. . . 4 ⊢ (𝜑 → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
126		tgfiss 22966	. . . 4 ⊢ (((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top ∧ (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) → (topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
127	30, 125, 126	syl2anc 585	. . 3 ⊢ (𝜑 → (topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
128	24, 127	eqsstrd 3957	. 2 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
129	9, 128	eqssd 3940	1 ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3390  Vcvv 3430   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  {csn 4568  ∪ cuni 4851   class class class wbr 5086   ↦ cmpt 5167   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  ficfi 9316  Basecbs 17170   ↾_s cress 17191  lecple 17218   ↾_t crest 17374  topGenctg 17391  ordTopcordt 17454  ODualcodu 18243   Proset cproset 18249  Posetcpo 18264  Tosetctos 18371  Topctop 22868  TopOnctopon 22885  TopBasesctb 22920

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fi 9317  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-dec 12636  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-ple 17231  df-rest 17376  df-topgen 17397  df-ordt 17456  df-odu 18244  df-proset 18251  df-poset 18270  df-toset 18372  df-top 22869  df-topon 22886  df-bases 22921

This theorem is referenced by: (None)