cnmpopc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnmpopc		Structured version Visualization version GIF version

Theorem cnmpopc 24444

Description: Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)

**Hypotheses**
Ref	Expression
cnmpopc.r	⊢ 𝑅 = (topGen‘ran (,))
cnmpopc.m	⊢ 𝑀 = (𝑅 ↾_t (𝐴[,]𝐵))
cnmpopc.n	⊢ 𝑁 = (𝑅 ↾_t (𝐵[,]𝐶))
cnmpopc.o	⊢ 𝑂 = (𝑅 ↾_t (𝐴[,]𝐶))
cnmpopc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
cnmpopc.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
cnmpopc.b	⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))
cnmpopc.j	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
cnmpopc.q	⊢ ((𝜑 ∧ (𝑥 = 𝐵 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐸)
cnmpopc.d	⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×_t 𝐽) Cn 𝐾))
cnmpopc.e	⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸) ∈ ((𝑁 ×_t 𝐽) Cn 𝐾))

**Assertion**
Ref	Expression
cnmpopc	⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑂 ×_t 𝐽) Cn 𝐾))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝐾,𝑦 𝜑,𝑥,𝑦 𝑥,𝑋,𝑦 Allowed substitution hints: 𝐷(𝑥,𝑦) 𝑅(𝑥,𝑦) 𝐸(𝑥,𝑦) 𝐽(𝑥,𝑦) 𝑀(𝑥,𝑦) 𝑁(𝑥,𝑦) 𝑂(𝑥,𝑦)

**Proof of Theorem cnmpopc**
Step	Hyp	Ref	Expression
1		eqid 2733	. 2 ⊢ ∪ (𝑂 ×_t 𝐽) = ∪ (𝑂 ×_t 𝐽)
2		eqid 2733	. 2 ⊢ ∪ 𝐾 = ∪ 𝐾
3		cnmpopc.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		cnmpopc.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5		iccssre 13406	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴[,]𝐶) ⊆ ℝ)
6	3, 4, 5	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐴[,]𝐶) ⊆ ℝ)
7		cnmpopc.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))
8	6, 7	sseldd 3984	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		icccld 24283	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,))))
10	3, 8, 9	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,))))
11		cnmpopc.r	. . . . . . 7 ⊢ 𝑅 = (topGen‘ran (,))
12	11	fveq2i 6895	. . . . . 6 ⊢ (Clsd‘𝑅) = (Clsd‘(topGen‘ran (,)))
13	10, 12	eleqtrrdi 2845	. . . . 5 ⊢ (𝜑 → (𝐴[,]𝐵) ∈ (Clsd‘𝑅))
14		ssun1 4173	. . . . . 6 ⊢ (𝐴[,]𝐵) ⊆ ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶))
15		iccsplit 13462	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ (𝐴[,]𝐶)) → (𝐴[,]𝐶) = ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶)))
16	3, 4, 7, 15	syl3anc 1372	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐶) = ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶)))
17	14, 16	sseqtrrid 4036	. . . . 5 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (𝐴[,]𝐶))
18		uniretop 24279	. . . . . . 7 ⊢ ℝ = ∪ (topGen‘ran (,))
19	11	unieqi 4922	. . . . . . 7 ⊢ ∪ 𝑅 = ∪ (topGen‘ran (,))
20	18, 19	eqtr4i 2764	. . . . . 6 ⊢ ℝ = ∪ 𝑅
21	20	restcldi 22677	. . . . 5 ⊢ (((𝐴[,]𝐶) ⊆ ℝ ∧ (𝐴[,]𝐵) ∈ (Clsd‘𝑅) ∧ (𝐴[,]𝐵) ⊆ (𝐴[,]𝐶)) → (𝐴[,]𝐵) ∈ (Clsd‘(𝑅 ↾_t (𝐴[,]𝐶))))
22	6, 13, 17, 21	syl3anc 1372	. . . 4 ⊢ (𝜑 → (𝐴[,]𝐵) ∈ (Clsd‘(𝑅 ↾_t (𝐴[,]𝐶))))
23		cnmpopc.o	. . . . 5 ⊢ 𝑂 = (𝑅 ↾_t (𝐴[,]𝐶))
24	23	fveq2i 6895	. . . 4 ⊢ (Clsd‘𝑂) = (Clsd‘(𝑅 ↾_t (𝐴[,]𝐶)))
25	22, 24	eleqtrrdi 2845	. . 3 ⊢ (𝜑 → (𝐴[,]𝐵) ∈ (Clsd‘𝑂))
26		cnmpopc.j	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
27		toponuni 22416	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
28	26, 27	syl 17	. . . 4 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
29		topontop 22415	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
30		eqid 2733	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
31	30	topcld 22539	. . . . 5 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ (Clsd‘𝐽))
32	26, 29, 31	3syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝐽 ∈ (Clsd‘𝐽))
33	28, 32	eqeltrd 2834	. . 3 ⊢ (𝜑 → 𝑋 ∈ (Clsd‘𝐽))
34		txcld 23107	. . 3 ⊢ (((𝐴[,]𝐵) ∈ (Clsd‘𝑂) ∧ 𝑋 ∈ (Clsd‘𝐽)) → ((𝐴[,]𝐵) × 𝑋) ∈ (Clsd‘(𝑂 ×_t 𝐽)))
35	25, 33, 34	syl2anc 585	. 2 ⊢ (𝜑 → ((𝐴[,]𝐵) × 𝑋) ∈ (Clsd‘(𝑂 ×_t 𝐽)))
36		icccld 24283	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵[,]𝐶) ∈ (Clsd‘(topGen‘ran (,))))
37	8, 4, 36	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐵[,]𝐶) ∈ (Clsd‘(topGen‘ran (,))))
38	37, 12	eleqtrrdi 2845	. . . . 5 ⊢ (𝜑 → (𝐵[,]𝐶) ∈ (Clsd‘𝑅))
39		ssun2 4174	. . . . . 6 ⊢ (𝐵[,]𝐶) ⊆ ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶))
40	39, 16	sseqtrrid 4036	. . . . 5 ⊢ (𝜑 → (𝐵[,]𝐶) ⊆ (𝐴[,]𝐶))
41	20	restcldi 22677	. . . . 5 ⊢ (((𝐴[,]𝐶) ⊆ ℝ ∧ (𝐵[,]𝐶) ∈ (Clsd‘𝑅) ∧ (𝐵[,]𝐶) ⊆ (𝐴[,]𝐶)) → (𝐵[,]𝐶) ∈ (Clsd‘(𝑅 ↾_t (𝐴[,]𝐶))))
42	6, 38, 40, 41	syl3anc 1372	. . . 4 ⊢ (𝜑 → (𝐵[,]𝐶) ∈ (Clsd‘(𝑅 ↾_t (𝐴[,]𝐶))))
43	42, 24	eleqtrrdi 2845	. . 3 ⊢ (𝜑 → (𝐵[,]𝐶) ∈ (Clsd‘𝑂))
44		txcld 23107	. . 3 ⊢ (((𝐵[,]𝐶) ∈ (Clsd‘𝑂) ∧ 𝑋 ∈ (Clsd‘𝐽)) → ((𝐵[,]𝐶) × 𝑋) ∈ (Clsd‘(𝑂 ×_t 𝐽)))
45	43, 33, 44	syl2anc 585	. 2 ⊢ (𝜑 → ((𝐵[,]𝐶) × 𝑋) ∈ (Clsd‘(𝑂 ×_t 𝐽)))
46	16	xpeq1d 5706	. . . 4 ⊢ (𝜑 → ((𝐴[,]𝐶) × 𝑋) = (((𝐴[,]𝐵) ∪ (𝐵[,]𝐶)) × 𝑋))
47		xpundir 5746	. . . 4 ⊢ (((𝐴[,]𝐵) ∪ (𝐵[,]𝐶)) × 𝑋) = (((𝐴[,]𝐵) × 𝑋) ∪ ((𝐵[,]𝐶) × 𝑋))
48	46, 47	eqtrdi 2789	. . 3 ⊢ (𝜑 → ((𝐴[,]𝐶) × 𝑋) = (((𝐴[,]𝐵) × 𝑋) ∪ ((𝐵[,]𝐶) × 𝑋)))
49		retopon 24280	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
50	11, 49	eqeltri 2830	. . . . . . 7 ⊢ 𝑅 ∈ (TopOn‘ℝ)
51		resttopon 22665	. . . . . . 7 ⊢ ((𝑅 ∈ (TopOn‘ℝ) ∧ (𝐴[,]𝐶) ⊆ ℝ) → (𝑅 ↾_t (𝐴[,]𝐶)) ∈ (TopOn‘(𝐴[,]𝐶)))
52	50, 6, 51	sylancr 588	. . . . . 6 ⊢ (𝜑 → (𝑅 ↾_t (𝐴[,]𝐶)) ∈ (TopOn‘(𝐴[,]𝐶)))
53	23, 52	eqeltrid 2838	. . . . 5 ⊢ (𝜑 → 𝑂 ∈ (TopOn‘(𝐴[,]𝐶)))
54		txtopon 23095	. . . . 5 ⊢ ((𝑂 ∈ (TopOn‘(𝐴[,]𝐶)) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝑂 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐶) × 𝑋)))
55	53, 26, 54	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑂 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐶) × 𝑋)))
56		toponuni 22416	. . . 4 ⊢ ((𝑂 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐶) × 𝑋)) → ((𝐴[,]𝐶) × 𝑋) = ∪ (𝑂 ×_t 𝐽))
57	55, 56	syl 17	. . 3 ⊢ (𝜑 → ((𝐴[,]𝐶) × 𝑋) = ∪ (𝑂 ×_t 𝐽))
58	48, 57	eqtr3d 2775	. 2 ⊢ (𝜑 → (((𝐴[,]𝐵) × 𝑋) ∪ ((𝐵[,]𝐶) × 𝑋)) = ∪ (𝑂 ×_t 𝐽))
59		cnmpopc.m	. . . . . . . . . 10 ⊢ 𝑀 = (𝑅 ↾_t (𝐴[,]𝐵))
60	17, 6	sstrd 3993	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
61		resttopon 22665	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ (TopOn‘ℝ) ∧ (𝐴[,]𝐵) ⊆ ℝ) → (𝑅 ↾_t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
62	50, 60, 61	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ↾_t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)))
63	59, 62	eqeltrid 2838	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (TopOn‘(𝐴[,]𝐵)))
64		txtopon 23095	. . . . . . . . 9 ⊢ ((𝑀 ∈ (TopOn‘(𝐴[,]𝐵)) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝑀 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐵) × 𝑋)))
65	63, 26, 64	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐵) × 𝑋)))
66		cnmpopc.d	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×_t 𝐽) Cn 𝐾))
67		cntop2 22745	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×_t 𝐽) Cn 𝐾) → 𝐾 ∈ Top)
68	66, 67	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Top)
69		toptopon2 22420	. . . . . . . . 9 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
70	68, 69	sylib 217	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾))
71		elicc2 13389	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
72	3, 8, 71	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
73	72	biimpa 478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
74	73	simp3d 1145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
75	74	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ 𝑋) → 𝑥 ≤ 𝐵)
76	75	iftrued 4537	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ 𝑋) → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐷)
77	76	mpoeq3dva 7486	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷))
78	77, 66	eqeltrd 2834	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑀 ×_t 𝐽) Cn 𝐾))
79		cnf2 22753	. . . . . . . 8 ⊢ (((𝑀 ×_t 𝐽) ∈ (TopOn‘((𝐴[,]𝐵) × 𝑋)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾) ∧ (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑀 ×_t 𝐽) Cn 𝐾)) → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐵) × 𝑋)⟶∪ 𝐾)
80	65, 70, 78, 79	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐵) × 𝑋)⟶∪ 𝐾)
81		eqid 2733	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸))
82	81	fmpo 8054	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾 ↔ (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐵) × 𝑋)⟶∪ 𝐾)
83	80, 82	sylibr 233	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾)
84		cnmpopc.n	. . . . . . . . . 10 ⊢ 𝑁 = (𝑅 ↾_t (𝐵[,]𝐶))
85	40, 6	sstrd 3993	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ)
86		resttopon 22665	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ (TopOn‘ℝ) ∧ (𝐵[,]𝐶) ⊆ ℝ) → (𝑅 ↾_t (𝐵[,]𝐶)) ∈ (TopOn‘(𝐵[,]𝐶)))
87	50, 85, 86	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ↾_t (𝐵[,]𝐶)) ∈ (TopOn‘(𝐵[,]𝐶)))
88	84, 87	eqeltrid 2838	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (TopOn‘(𝐵[,]𝐶)))
89		txtopon 23095	. . . . . . . . 9 ⊢ ((𝑁 ∈ (TopOn‘(𝐵[,]𝐶)) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝑁 ×_t 𝐽) ∈ (TopOn‘((𝐵[,]𝐶) × 𝑋)))
90	88, 26, 89	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑁 ×_t 𝐽) ∈ (TopOn‘((𝐵[,]𝐶) × 𝑋)))
91		elicc2 13389	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑥 ∈ (𝐵[,]𝐶) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐶)))
92	8, 4, 91	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐶)))
93	92	biimpa 478	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 ≤ 𝐶))
94	93	simp2d 1144	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → 𝐵 ≤ 𝑥)
95	94	biantrud 533	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → (𝑥 ≤ 𝐵 ↔ (𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥)))
96	93	simp1d 1143	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → 𝑥 ∈ ℝ)
97	8	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → 𝐵 ∈ ℝ)
98	96, 97	letri3d 11356	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → (𝑥 = 𝐵 ↔ (𝑥 ≤ 𝐵 ∧ 𝐵 ≤ 𝑥)))
99	95, 98	bitr4d 282	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶)) → (𝑥 ≤ 𝐵 ↔ 𝑥 = 𝐵))
100	99	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶) ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝐵 ↔ 𝑥 = 𝐵))
101		cnmpopc.q	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 = 𝐵 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐸)
102	101	ancom2s 649	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 = 𝐵)) → 𝐷 = 𝐸)
103	102	ifeq1d 4548	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 = 𝐵)) → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = if(𝑥 ≤ 𝐵, 𝐸, 𝐸))
104		ifid 4569	. . . . . . . . . . . . . . 15 ⊢ if(𝑥 ≤ 𝐵, 𝐸, 𝐸) = 𝐸
105	103, 104	eqtrdi 2789	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 = 𝐵)) → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸)
106	105	expr 458	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑥 = 𝐵 → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸))
107	106	3adant2 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶) ∧ 𝑦 ∈ 𝑋) → (𝑥 = 𝐵 → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸))
108	100, 107	sylbid 239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶) ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝐵 → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸))
109		iffalse 4538	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ≤ 𝐵 → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸)
110	108, 109	pm2.61d1 180	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,]𝐶) ∧ 𝑦 ∈ 𝑋) → if(𝑥 ≤ 𝐵, 𝐷, 𝐸) = 𝐸)
111	110	mpoeq3dva 7486	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) = (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸))
112		cnmpopc.e	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸) ∈ ((𝑁 ×_t 𝐽) Cn 𝐾))
113	111, 112	eqeltrd 2834	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑁 ×_t 𝐽) Cn 𝐾))
114		cnf2 22753	. . . . . . . 8 ⊢ (((𝑁 ×_t 𝐽) ∈ (TopOn‘((𝐵[,]𝐶) × 𝑋)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾) ∧ (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑁 ×_t 𝐽) Cn 𝐾)) → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐵[,]𝐶) × 𝑋)⟶∪ 𝐾)
115	90, 70, 113, 114	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐵[,]𝐶) × 𝑋)⟶∪ 𝐾)
116		eqid 2733	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) = (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸))
117	116	fmpo 8054	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾 ↔ (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐵[,]𝐶) × 𝑋)⟶∪ 𝐾)
118	115, 117	sylibr 233	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾)
119		ralun 4193	. . . . . 6 ⊢ ((∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾 ∧ ∀𝑥 ∈ (𝐵[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾) → ∀𝑥 ∈ ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶))∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾)
120	83, 118, 119	syl2anc 585	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶))∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾)
121	16	raleqdv 3326	. . . . 5 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾 ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∪ (𝐵[,]𝐶))∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾))
122	120, 121	mpbird 257	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾)
123		eqid 2733	. . . . 5 ⊢ (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) = (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸))
124	123	fmpo 8054	. . . 4 ⊢ (∀𝑥 ∈ (𝐴[,]𝐶)∀𝑦 ∈ 𝑋 if(𝑥 ≤ 𝐵, 𝐷, 𝐸) ∈ ∪ 𝐾 ↔ (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐶) × 𝑋)⟶∪ 𝐾)
125	122, 124	sylib 217	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐶) × 𝑋)⟶∪ 𝐾)
126	57	feq2d 6704	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):((𝐴[,]𝐶) × 𝑋)⟶∪ 𝐾 ↔ (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):∪ (𝑂 ×_t 𝐽)⟶∪ 𝐾))
127	125, 126	mpbid 231	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)):∪ (𝑂 ×_t 𝐽)⟶∪ 𝐾)
128		ssid 4005	. . . 4 ⊢ 𝑋 ⊆ 𝑋
129		resmpo 7528	. . . 4 ⊢ (((𝐴[,]𝐵) ⊆ (𝐴[,]𝐶) ∧ 𝑋 ⊆ 𝑋) → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐴[,]𝐵) × 𝑋)) = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)))
130	17, 128, 129	sylancl 587	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐴[,]𝐵) × 𝑋)) = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)))
131		retop 24278	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ Top
132	11, 131	eqeltri 2830	. . . . . . . . 9 ⊢ 𝑅 ∈ Top
133		ovex 7442	. . . . . . . . 9 ⊢ (𝐴[,]𝐶) ∈ V
134		resttop 22664	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ (𝐴[,]𝐶) ∈ V) → (𝑅 ↾_t (𝐴[,]𝐶)) ∈ Top)
135	132, 133, 134	mp2an 691	. . . . . . . 8 ⊢ (𝑅 ↾_t (𝐴[,]𝐶)) ∈ Top
136	23, 135	eqeltri 2830	. . . . . . 7 ⊢ 𝑂 ∈ Top
137	136	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑂 ∈ Top)
138		ovexd 7444	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ∈ V)
139		txrest 23135	. . . . . 6 ⊢ (((𝑂 ∈ Top ∧ 𝐽 ∈ (TopOn‘𝑋)) ∧ ((𝐴[,]𝐵) ∈ V ∧ 𝑋 ∈ (Clsd‘𝐽))) → ((𝑂 ×_t 𝐽) ↾_t ((𝐴[,]𝐵) × 𝑋)) = ((𝑂 ↾_t (𝐴[,]𝐵)) ×_t (𝐽 ↾_t 𝑋)))
140	137, 26, 138, 33, 139	syl22anc 838	. . . . 5 ⊢ (𝜑 → ((𝑂 ×_t 𝐽) ↾_t ((𝐴[,]𝐵) × 𝑋)) = ((𝑂 ↾_t (𝐴[,]𝐵)) ×_t (𝐽 ↾_t 𝑋)))
141	132	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Top)
142		ovexd 7444	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐶) ∈ V)
143		restabs 22669	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ (𝐴[,]𝐵) ⊆ (𝐴[,]𝐶) ∧ (𝐴[,]𝐶) ∈ V) → ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐴[,]𝐵)) = (𝑅 ↾_t (𝐴[,]𝐵)))
144	141, 17, 142, 143	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐴[,]𝐵)) = (𝑅 ↾_t (𝐴[,]𝐵)))
145	23	oveq1i 7419	. . . . . . 7 ⊢ (𝑂 ↾_t (𝐴[,]𝐵)) = ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐴[,]𝐵))
146	144, 145, 59	3eqtr4g 2798	. . . . . 6 ⊢ (𝜑 → (𝑂 ↾_t (𝐴[,]𝐵)) = 𝑀)
147	28	oveq2d 7425	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾_t 𝑋) = (𝐽 ↾_t ∪ 𝐽))
148	30	restid 17379	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ↾_t ∪ 𝐽) = 𝐽)
149	26, 148	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾_t ∪ 𝐽) = 𝐽)
150	147, 149	eqtrd 2773	. . . . . 6 ⊢ (𝜑 → (𝐽 ↾_t 𝑋) = 𝐽)
151	146, 150	oveq12d 7427	. . . . 5 ⊢ (𝜑 → ((𝑂 ↾_t (𝐴[,]𝐵)) ×_t (𝐽 ↾_t 𝑋)) = (𝑀 ×_t 𝐽))
152	140, 151	eqtrd 2773	. . . 4 ⊢ (𝜑 → ((𝑂 ×_t 𝐽) ↾_t ((𝐴[,]𝐵) × 𝑋)) = (𝑀 ×_t 𝐽))
153	152	oveq1d 7424	. . 3 ⊢ (𝜑 → (((𝑂 ×_t 𝐽) ↾_t ((𝐴[,]𝐵) × 𝑋)) Cn 𝐾) = ((𝑀 ×_t 𝐽) Cn 𝐾))
154	78, 130, 153	3eltr4d 2849	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐴[,]𝐵) × 𝑋)) ∈ (((𝑂 ×_t 𝐽) ↾_t ((𝐴[,]𝐵) × 𝑋)) Cn 𝐾))
155		resmpo 7528	. . . 4 ⊢ (((𝐵[,]𝐶) ⊆ (𝐴[,]𝐶) ∧ 𝑋 ⊆ 𝑋) → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐵[,]𝐶) × 𝑋)) = (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)))
156	40, 128, 155	sylancl 587	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐵[,]𝐶) × 𝑋)) = (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)))
157		ovexd 7444	. . . . . 6 ⊢ (𝜑 → (𝐵[,]𝐶) ∈ V)
158		txrest 23135	. . . . . 6 ⊢ (((𝑂 ∈ Top ∧ 𝐽 ∈ (TopOn‘𝑋)) ∧ ((𝐵[,]𝐶) ∈ V ∧ 𝑋 ∈ (Clsd‘𝐽))) → ((𝑂 ×_t 𝐽) ↾_t ((𝐵[,]𝐶) × 𝑋)) = ((𝑂 ↾_t (𝐵[,]𝐶)) ×_t (𝐽 ↾_t 𝑋)))
159	137, 26, 157, 33, 158	syl22anc 838	. . . . 5 ⊢ (𝜑 → ((𝑂 ×_t 𝐽) ↾_t ((𝐵[,]𝐶) × 𝑋)) = ((𝑂 ↾_t (𝐵[,]𝐶)) ×_t (𝐽 ↾_t 𝑋)))
160		restabs 22669	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ (𝐵[,]𝐶) ⊆ (𝐴[,]𝐶) ∧ (𝐴[,]𝐶) ∈ V) → ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐵[,]𝐶)) = (𝑅 ↾_t (𝐵[,]𝐶)))
161	141, 40, 142, 160	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐵[,]𝐶)) = (𝑅 ↾_t (𝐵[,]𝐶)))
162	23	oveq1i 7419	. . . . . . 7 ⊢ (𝑂 ↾_t (𝐵[,]𝐶)) = ((𝑅 ↾_t (𝐴[,]𝐶)) ↾_t (𝐵[,]𝐶))
163	161, 162, 84	3eqtr4g 2798	. . . . . 6 ⊢ (𝜑 → (𝑂 ↾_t (𝐵[,]𝐶)) = 𝑁)
164	163, 150	oveq12d 7427	. . . . 5 ⊢ (𝜑 → ((𝑂 ↾_t (𝐵[,]𝐶)) ×_t (𝐽 ↾_t 𝑋)) = (𝑁 ×_t 𝐽))
165	159, 164	eqtrd 2773	. . . 4 ⊢ (𝜑 → ((𝑂 ×_t 𝐽) ↾_t ((𝐵[,]𝐶) × 𝑋)) = (𝑁 ×_t 𝐽))
166	165	oveq1d 7424	. . 3 ⊢ (𝜑 → (((𝑂 ×_t 𝐽) ↾_t ((𝐵[,]𝐶) × 𝑋)) Cn 𝐾) = ((𝑁 ×_t 𝐽) Cn 𝐾))
167	113, 156, 166	3eltr4d 2849	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ↾ ((𝐵[,]𝐶) × 𝑋)) ∈ (((𝑂 ×_t 𝐽) ↾_t ((𝐵[,]𝐶) × 𝑋)) Cn 𝐾))
168	1, 2, 35, 45, 58, 127, 154, 167	paste 22798	1 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑂 ×_t 𝐽) Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 Vcvv 3475 ∪ cun 3947 ⊆ wss 3949 ifcif 4529 ∪ cuni 4909 class class class wbr 5149 × cxp 5675 ran crn 5678 ↾ cres 5679 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 ℝcr 11109 ≤ cle 11249 (,)cioo 13324 [,]cicc 13327 ↾_t crest 17366 topGenctg 17383 Topctop 22395 TopOnctopon 22412 Clsdccld 22520 Cn ccn 22728 ×_t ctx 23064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fi 9406 df-sup 9437 df-inf 9438 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-n0 12473 df-z 12559 df-uz 12823 df-q 12933 df-ioo 13328 df-icc 13331 df-rest 17368 df-topgen 17389 df-top 22396 df-topon 22413 df-bases 22449 df-cld 22523 df-cn 22731 df-tx 23066

This theorem is referenced by: htpycc 24496 pcocn 24533 pcohtpylem 24535 pcopt 24538 pcopt2 24539 pcoass 24540 pcorevlem 24542

W3C validator