sbthlem1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > sbthlem1		GIF version

Theorem sbthlem1 6204

Description: Lemma for sbth 6207. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)

**Hypotheses**
Ref	Expression
sbthlem1.1	⊢ R ∈ V
sbthlem1.2	⊢ X ∈ V
sbthlem1.3	⊢ G = Clos1 ((X ∖ ran R), R)
sbthlem1.4	⊢ A = (X ∩ G)
sbthlem1.5	⊢ B = (X ∖ G)
sbthlem1.6	⊢ C = (ran R ∩ G)
sbthlem1.7	⊢ D = (ran R ∖ G)

**Assertion**
Ref	Expression
sbthlem1	⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ran R ≈ X)

**Proof of Theorem sbthlem1**
Step	Hyp	Ref	Expression
1		df-f1 4793	. . . . . . . . 9 ⊢ (R:dom R–1-1→ran R ↔ (R:dom R–→ran R ∧ Fun ^◡R))
2		ssid 3291	. . . . . . . . . . . 12 ⊢ ran R ⊆ ran R
3		df-f 4792	. . . . . . . . . . . 12 ⊢ (R:dom R–→ran R ↔ (R Fn dom R ∧ ran R ⊆ ran R))
4	2, 3	mpbiran2 885	. . . . . . . . . . 11 ⊢ (R:dom R–→ran R ↔ R Fn dom R)
5		funfn 5137	. . . . . . . . . . 11 ⊢ (Fun R ↔ R Fn dom R)
6	4, 5	bitr4i 243	. . . . . . . . . 10 ⊢ (R:dom R–→ran R ↔ Fun R)
7	6	anbi1i 676	. . . . . . . . 9 ⊢ ((R:dom R–→ran R ∧ Fun ^◡R) ↔ (Fun R ∧ Fun ^◡R))
8	1, 7	bitri 240	. . . . . . . 8 ⊢ (R:dom R–1-1→ran R ↔ (Fun R ∧ Fun ^◡R))
9	8	biimpri 197	. . . . . . 7 ⊢ ((Fun R ∧ Fun ^◡R) → R:dom R–1-1→ran R)
10		sbthlem1.4	. . . . . . . . 9 ⊢ A = (X ∩ G)
11		inss1 3476	. . . . . . . . . 10 ⊢ (X ∩ G) ⊆ X
12		sstr 3281	. . . . . . . . . 10 ⊢ (((X ∩ G) ⊆ X ∧ X ⊆ dom R) → (X ∩ G) ⊆ dom R)
13	11, 12	mpan 651	. . . . . . . . 9 ⊢ (X ⊆ dom R → (X ∩ G) ⊆ dom R)
14	10, 13	syl5eqss 3316	. . . . . . . 8 ⊢ (X ⊆ dom R → A ⊆ dom R)
15	14	adantr 451	. . . . . . 7 ⊢ ((X ⊆ dom R ∧ ran R ⊆ X) → A ⊆ dom R)
16		f1ores 5301	. . . . . . 7 ⊢ ((R:dom R–1-1→ran R ∧ A ⊆ dom R) → (R ↾ A):A–1-1-onto→(R “ A))
17	9, 15, 16	syl2an 463	. . . . . 6 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R ↾ A):A–1-1-onto→(R “ A))
18		sbthlem1.1	. . . . . . . 8 ⊢ R ∈ V
19		sbthlem1.2	. . . . . . . . . 10 ⊢ X ∈ V
20		sbthlem1.3	. . . . . . . . . . 11 ⊢ G = Clos1 ((X ∖ ran R), R)
21	18	rnex 5108	. . . . . . . . . . . . 13 ⊢ ran R ∈ V
22	19, 21	difex 4108	. . . . . . . . . . . 12 ⊢ (X ∖ ran R) ∈ V
23	22, 18	clos1ex 5877	. . . . . . . . . . 11 ⊢ Clos1 ((X ∖ ran R), R) ∈ V
24	20, 23	eqeltri 2423	. . . . . . . . . 10 ⊢ G ∈ V
25	19, 24	inex 4106	. . . . . . . . 9 ⊢ (X ∩ G) ∈ V
26	10, 25	eqeltri 2423	. . . . . . . 8 ⊢ A ∈ V
27	18, 26	resex 5118	. . . . . . 7 ⊢ (R ↾ A) ∈ V
28	27	f1oen 6034	. . . . . 6 ⊢ ((R ↾ A):A–1-1-onto→(R “ A) → A ≈ (R “ A))
29	17, 28	syl 15	. . . . 5 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → A ≈ (R “ A))
30		sbthlem1.6	. . . . . . . . 9 ⊢ C = (ran R ∩ G)
31	22, 18, 20	clos1baseima 5884	. . . . . . . . . 10 ⊢ G = ((X ∖ ran R) ∪ (R “ G))
32	31	ineq2i 3455	. . . . . . . . 9 ⊢ (ran R ∩ G) = (ran R ∩ ((X ∖ ran R) ∪ (R “ G)))
33		indi 3502	. . . . . . . . . 10 ⊢ (ran R ∩ ((X ∖ ran R) ∪ (R “ G))) = ((ran R ∩ (X ∖ ran R)) ∪ (ran R ∩ (R “ G)))
34		disjdif 3623	. . . . . . . . . . 11 ⊢ (ran R ∩ (X ∖ ran R)) = ∅
35	34	uneq1i 3415	. . . . . . . . . 10 ⊢ ((ran R ∩ (X ∖ ran R)) ∪ (ran R ∩ (R “ G))) = (∅ ∪ (ran R ∩ (R “ G)))
36		uncom 3409	. . . . . . . . . . 11 ⊢ (∅ ∪ (ran R ∩ (R “ G))) = ((ran R ∩ (R “ G)) ∪ ∅)
37		un0 3576	. . . . . . . . . . 11 ⊢ ((ran R ∩ (R “ G)) ∪ ∅) = (ran R ∩ (R “ G))
38	36, 37	eqtri 2373	. . . . . . . . . 10 ⊢ (∅ ∪ (ran R ∩ (R “ G))) = (ran R ∩ (R “ G))
39	33, 35, 38	3eqtri 2377	. . . . . . . . 9 ⊢ (ran R ∩ ((X ∖ ran R) ∪ (R “ G))) = (ran R ∩ (R “ G))
40	30, 32, 39	3eqtri 2377	. . . . . . . 8 ⊢ C = (ran R ∩ (R “ G))
41		inss2 3477	. . . . . . . . 9 ⊢ (ran R ∩ (R “ G)) ⊆ (R “ G)
42	41	a1i 10	. . . . . . . 8 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (ran R ∩ (R “ G)) ⊆ (R “ G))
43	40, 42	syl5eqss 3316	. . . . . . 7 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → C ⊆ (R “ G))
44		imassrn 5010	. . . . . . . . . . . . . 14 ⊢ (R “ G) ⊆ ran R
45		simprr 733	. . . . . . . . . . . . . 14 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ran R ⊆ X)
46	44, 45	syl5ss 3284	. . . . . . . . . . . . 13 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R “ G) ⊆ X)
47		difss 3394	. . . . . . . . . . . . 13 ⊢ (X ∖ ran R) ⊆ X
48	46, 47	jctil 523	. . . . . . . . . . . 12 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ((X ∖ ran R) ⊆ X ∧ (R “ G) ⊆ X))
49		unss 3438	. . . . . . . . . . . 12 ⊢ (((X ∖ ran R) ⊆ X ∧ (R “ G) ⊆ X) ↔ ((X ∖ ran R) ∪ (R “ G)) ⊆ X)
50	48, 49	sylib 188	. . . . . . . . . . 11 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ((X ∖ ran R) ∪ (R “ G)) ⊆ X)
51	31, 50	syl5eqss 3316	. . . . . . . . . 10 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → G ⊆ X)
52		sseqin2 3475	. . . . . . . . . 10 ⊢ (G ⊆ X ↔ (X ∩ G) = G)
53	51, 52	sylib 188	. . . . . . . . 9 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (X ∩ G) = G)
54	10, 53	syl5eq 2397	. . . . . . . 8 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → A = G)
55	54	imaeq2d 4943	. . . . . . 7 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R “ A) = (R “ G))
56	43, 55	sseqtr4d 3309	. . . . . 6 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → C ⊆ (R “ A))
57		ssun2 3428	. . . . . . . . . . 11 ⊢ (R “ G) ⊆ ((X ∖ ran R) ∪ (R “ G))
58	57, 31	sseqtr4i 3305	. . . . . . . . . 10 ⊢ (R “ G) ⊆ G
59	55	sseq1d 3299	. . . . . . . . . 10 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ((R “ A) ⊆ G ↔ (R “ G) ⊆ G))
60	58, 59	mpbiri 224	. . . . . . . . 9 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R “ A) ⊆ G)
61		imassrn 5010	. . . . . . . . 9 ⊢ (R “ A) ⊆ ran R
62	60, 61	jctil 523	. . . . . . . 8 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ((R “ A) ⊆ ran R ∧ (R “ A) ⊆ G))
63		ssin 3478	. . . . . . . 8 ⊢ (((R “ A) ⊆ ran R ∧ (R “ A) ⊆ G) ↔ (R “ A) ⊆ (ran R ∩ G))
64	62, 63	sylib 188	. . . . . . 7 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R “ A) ⊆ (ran R ∩ G))
65	64, 30	syl6sseqr 3319	. . . . . 6 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (R “ A) ⊆ C)
66	56, 65	eqssd 3290	. . . . 5 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → C = (R “ A))
67	29, 66	breqtrrd 4666	. . . 4 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → A ≈ C)
68		sbthlem1.5	. . . . . . 7 ⊢ B = (X ∖ G)
69	19, 24	difex 4108	. . . . . . 7 ⊢ (X ∖ G) ∈ V
70	68, 69	eqeltri 2423	. . . . . 6 ⊢ B ∈ V
71	70	enrflx 6036	. . . . 5 ⊢ B ≈ B
72		difsscompl 3550	. . . . . . . . . 10 ⊢ (X ∖ G) ⊆ ∼ G
73	72	a1i 10	. . . . . . . . 9 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (X ∖ G) ⊆ ∼ G)
74		df-dif 3216	. . . . . . . . . . 11 ⊢ (X ∖ G) = (X ∩ ∼ G)
75	20	clos1base 5879	. . . . . . . . . . . . . 14 ⊢ (X ∖ ran R) ⊆ G
76		sscon34 3662	. . . . . . . . . . . . . 14 ⊢ ((X ∖ ran R) ⊆ G ↔ ∼ G ⊆ ∼ (X ∖ ran R))
77	75, 76	mpbi 199	. . . . . . . . . . . . 13 ⊢ ∼ G ⊆ ∼ (X ∖ ran R)
78		df-dif 3216	. . . . . . . . . . . . . . 15 ⊢ (X ∖ ran R) = (X ∩ ∼ ran R)
79	78	compleqi 3245	. . . . . . . . . . . . . 14 ⊢ ∼ (X ∖ ran R) = ∼ (X ∩ ∼ ran R)
80		iinun 3549	. . . . . . . . . . . . . 14 ⊢ ∼ (X ∩ ∼ ran R) = ( ∼ X ∪ ∼ ∼ ran R)
81		dblcompl 3228	. . . . . . . . . . . . . . 15 ⊢ ∼ ∼ ran R = ran R
82	81	uneq2i 3416	. . . . . . . . . . . . . 14 ⊢ ( ∼ X ∪ ∼ ∼ ran R) = ( ∼ X ∪ ran R)
83	79, 80, 82	3eqtri 2377	. . . . . . . . . . . . 13 ⊢ ∼ (X ∖ ran R) = ( ∼ X ∪ ran R)
84	77, 83	sseqtri 3304	. . . . . . . . . . . 12 ⊢ ∼ G ⊆ ( ∼ X ∪ ran R)
85		sslin 3482	. . . . . . . . . . . 12 ⊢ ( ∼ G ⊆ ( ∼ X ∪ ran R) → (X ∩ ∼ G) ⊆ (X ∩ ( ∼ X ∪ ran R)))
86	84, 85	ax-mp 5	. . . . . . . . . . 11 ⊢ (X ∩ ∼ G) ⊆ (X ∩ ( ∼ X ∪ ran R))
87	74, 86	eqsstri 3302	. . . . . . . . . 10 ⊢ (X ∖ G) ⊆ (X ∩ ( ∼ X ∪ ran R))
88		indi 3502	. . . . . . . . . . . 12 ⊢ (X ∩ ( ∼ X ∪ ran R)) = ((X ∩ ∼ X) ∪ (X ∩ ran R))
89		incompl 4074	. . . . . . . . . . . . 13 ⊢ (X ∩ ∼ X) = ∅
90	89	uneq1i 3415	. . . . . . . . . . . 12 ⊢ ((X ∩ ∼ X) ∪ (X ∩ ran R)) = (∅ ∪ (X ∩ ran R))
91		uncom 3409	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (X ∩ ran R)) = ((X ∩ ran R) ∪ ∅)
92		un0 3576	. . . . . . . . . . . . 13 ⊢ ((X ∩ ran R) ∪ ∅) = (X ∩ ran R)
93	91, 92	eqtri 2373	. . . . . . . . . . . 12 ⊢ (∅ ∪ (X ∩ ran R)) = (X ∩ ran R)
94	88, 90, 93	3eqtri 2377	. . . . . . . . . . 11 ⊢ (X ∩ ( ∼ X ∪ ran R)) = (X ∩ ran R)
95		inss2 3477	. . . . . . . . . . 11 ⊢ (X ∩ ran R) ⊆ ran R
96	94, 95	eqsstri 3302	. . . . . . . . . 10 ⊢ (X ∩ ( ∼ X ∪ ran R)) ⊆ ran R
97	87, 96	sstri 3282	. . . . . . . . 9 ⊢ (X ∖ G) ⊆ ran R
98	73, 97	jctil 523	. . . . . . . 8 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ((X ∖ G) ⊆ ran R ∧ (X ∖ G) ⊆ ∼ G))
99		ssin 3478	. . . . . . . 8 ⊢ (((X ∖ G) ⊆ ran R ∧ (X ∖ G) ⊆ ∼ G) ↔ (X ∖ G) ⊆ (ran R ∩ ∼ G))
100	98, 99	sylib 188	. . . . . . 7 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (X ∖ G) ⊆ (ran R ∩ ∼ G))
101		sbthlem1.7	. . . . . . . 8 ⊢ D = (ran R ∖ G)
102		df-dif 3216	. . . . . . . 8 ⊢ (ran R ∖ G) = (ran R ∩ ∼ G)
103	101, 102	eqtri 2373	. . . . . . 7 ⊢ D = (ran R ∩ ∼ G)
104	100, 68, 103	3sstr4g 3313	. . . . . 6 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → B ⊆ D)
105		ssdif 3402	. . . . . . . 8 ⊢ (ran R ⊆ X → (ran R ∖ G) ⊆ (X ∖ G))
106	45, 105	syl 15	. . . . . . 7 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (ran R ∖ G) ⊆ (X ∖ G))
107	106, 101, 68	3sstr4g 3313	. . . . . 6 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → D ⊆ B)
108	104, 107	eqssd 3290	. . . . 5 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → B = D)
109	71, 108	syl5breq 4675	. . . 4 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → B ≈ D)
110	10, 68	ineq12i 3456	. . . . . 6 ⊢ (A ∩ B) = ((X ∩ G) ∩ (X ∖ G))
111		inindif 4076	. . . . . 6 ⊢ ((X ∩ G) ∩ (X ∖ G)) = ∅
112	110, 111	eqtri 2373	. . . . 5 ⊢ (A ∩ B) = ∅
113	30, 101	ineq12i 3456	. . . . . 6 ⊢ (C ∩ D) = ((ran R ∩ G) ∩ (ran R ∖ G))
114		inindif 4076	. . . . . 6 ⊢ ((ran R ∩ G) ∩ (ran R ∖ G)) = ∅
115	113, 114	eqtri 2373	. . . . 5 ⊢ (C ∩ D) = ∅
116		unen 6049	. . . . 5 ⊢ (((A ≈ C ∧ B ≈ D) ∧ ((A ∩ B) = ∅ ∧ (C ∩ D) = ∅)) → (A ∪ B) ≈ (C ∪ D))
117	112, 115, 116	mpanr12 666	. . . 4 ⊢ ((A ≈ C ∧ B ≈ D) → (A ∪ B) ≈ (C ∪ D))
118	67, 109, 117	syl2anc 642	. . 3 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (A ∪ B) ≈ (C ∪ D))
119		ensym 6038	. . 3 ⊢ ((A ∪ B) ≈ (C ∪ D) ↔ (C ∪ D) ≈ (A ∪ B))
120	118, 119	sylib 188	. 2 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → (C ∪ D) ≈ (A ∪ B))
121	30, 101	uneq12i 3417	. . 3 ⊢ (C ∪ D) = ((ran R ∩ G) ∪ (ran R ∖ G))
122		inundif 3629	. . 3 ⊢ ((ran R ∩ G) ∪ (ran R ∖ G)) = ran R
123	121, 122	eqtri 2373	. 2 ⊢ (C ∪ D) = ran R
124	10, 68	uneq12i 3417	. . 3 ⊢ (A ∪ B) = ((X ∩ G) ∪ (X ∖ G))
125		inundif 3629	. . 3 ⊢ ((X ∩ G) ∪ (X ∖ G)) = X
126	124, 125	eqtri 2373	. 2 ⊢ (A ∪ B) = X
127	120, 123, 126	3brtr3g 4671	1 ⊢ (((Fun R ∧ Fun ^◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ran R ≈ X)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 358 = wceq 1642 ∈ wcel 1710 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊆ wss 3258 ∅c0 3551 class class class wbr 4640 “ cima 4723 ^◡ccnv 4772 dom cdm 4773 ran crn 4774 ↾ cres 4775 Fun wfun 4776 Fn wfn 4777 –→wf 4778 –1-1→wf1 4779 –1-1-onto→wf1o 4781 Clos1 cclos1 5873 ≈ cen 6029

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-13 1712 ax-14 1714 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This proof depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-id 4768 df-xp 4785 df-cnv 4786 df-rn 4787 df-dm 4788 df-res 4789 df-fun 4790 df-fn 4791 df-f 4792 df-f1 4793 df-fo 4794 df-f1o 4795 df-2nd 4798 df-txp 5737 df-fix 5741 df-ins2 5751 df-ins3 5753 df-image 5755 df-clos1 5874 df-en 6030

This theorem is used by: sbthlem2 6205

W3C validator