Theorem fun11iun 5305

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)

Hypotheses

Ref	Expression
fun11iun.1	⊢ (x = y → B = C)
fun11iun.2	⊢ B ∈ V

Assertion

Ref	Expression
fun11iun	⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∪x ∈ A B:∪x ∈ A D–1-1→S)

Distinct variable groups:   x,A   y,A   y,B   x,C   x,S

Allowed substitution hints:   B(x)   C(y)   D(x,y)   S(y)

Proof of Theorem fun11iun

Dummy variables u v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2862	. . . . . . . . . 10 ⊢ u ∈ V
2		eqeq1 2359	. . . . . . . . . . 11 ⊢ (z = u → (z = B ↔ u = B))
3	2	rexbidv 2635	. . . . . . . . . 10 ⊢ (z = u → (∃x ∈ A z = B ↔ ∃x ∈ A u = B))
4	1, 3	elab 2985	. . . . . . . . 9 ⊢ (u ∈ {z ∣ ∃x ∈ A z = B} ↔ ∃x ∈ A u = B)
5		r19.29 2754	. . . . . . . . . 10 ⊢ ((∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ ∃x ∈ A u = B) → ∃x ∈ A ((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B))
6		nfv 1619	. . . . . . . . . . . 12 ⊢ Ⅎx(Fun u ∧ Fun ◡u)
7		nfre1 2670	. . . . . . . . . . . . . 14 ⊢ Ⅎx∃x ∈ A z = B
8	7	nfab 2493	. . . . . . . . . . . . 13 ⊢ Ⅎx{z ∣ ∃x ∈ A z = B}
9		nfv 1619	. . . . . . . . . . . . 13 ⊢ Ⅎx(u ⊆ v ∨ v ⊆ u)
10	8, 9	nfral 2667	. . . . . . . . . . . 12 ⊢ Ⅎx∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)
11	6, 10	nfan 1824	. . . . . . . . . . 11 ⊢ Ⅎx((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u))
12		f1eq1 5253	. . . . . . . . . . . . . . . 16 ⊢ (u = B → (u:D–1-1→S ↔ B:D–1-1→S))
13	12	biimparc 473	. . . . . . . . . . . . . . 15 ⊢ ((B:D–1-1→S ∧ u = B) → u:D–1-1→S)
14		f1fun 5260	. . . . . . . . . . . . . . . 16 ⊢ (u:D–1-1→S → Fun u)
15		df-f1 4792	. . . . . . . . . . . . . . . . 17 ⊢ (u:D–1-1→S ↔ (u:D–→S ∧ Fun ◡u))
16	15	simprbi 450	. . . . . . . . . . . . . . . 16 ⊢ (u:D–1-1→S → Fun ◡u)
17	14, 16	jca 518	. . . . . . . . . . . . . . 15 ⊢ (u:D–1-1→S → (Fun u ∧ Fun ◡u))
18	13, 17	syl 15	. . . . . . . . . . . . . 14 ⊢ ((B:D–1-1→S ∧ u = B) → (Fun u ∧ Fun ◡u))
19	18	adantlr 695	. . . . . . . . . . . . 13 ⊢ (((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B) → (Fun u ∧ Fun ◡u))
20		vex 2862	. . . . . . . . . . . . . . . . 17 ⊢ v ∈ V
21		eqeq1 2359	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = v → (z = B ↔ v = B))
22	21	rexbidv 2635	. . . . . . . . . . . . . . . . . 18 ⊢ (z = v → (∃x ∈ A z = B ↔ ∃x ∈ A v = B))
23		fun11iun.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = y → B = C)
24	23	eqeq2d 2364	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = y → (v = B ↔ v = C))
25	24	cbvrexv 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x ∈ A v = B ↔ ∃y ∈ A v = C)
26	22, 25	syl6bb 252	. . . . . . . . . . . . . . . . 17 ⊢ (z = v → (∃x ∈ A z = B ↔ ∃y ∈ A v = C))
27	20, 26	elab 2985	. . . . . . . . . . . . . . . 16 ⊢ (v ∈ {z ∣ ∃x ∈ A z = B} ↔ ∃y ∈ A v = C)
28		r19.29 2754	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀y ∈ A (B ⊆ C ∨ C ⊆ B) ∧ ∃y ∈ A v = C) → ∃y ∈ A ((B ⊆ C ∨ C ⊆ B) ∧ v = C))
29		sseq12 3294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((u = B ∧ v = C) → (u ⊆ v ↔ B ⊆ C))
30	29	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((v = C ∧ u = B) → (u ⊆ v ↔ B ⊆ C))
31		sseq12 3294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((v = C ∧ u = B) → (v ⊆ u ↔ C ⊆ B))
32	30, 31	orbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((v = C ∧ u = B) → ((u ⊆ v ∨ v ⊆ u) ↔ (B ⊆ C ∨ C ⊆ B)))
33	32	biimprcd 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((B ⊆ C ∨ C ⊆ B) → ((v = C ∧ u = B) → (u ⊆ v ∨ v ⊆ u)))
34	33	expdimp 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((B ⊆ C ∨ C ⊆ B) ∧ v = C) → (u = B → (u ⊆ v ∨ v ⊆ u)))
35	34	rexlimivw 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃y ∈ A ((B ⊆ C ∨ C ⊆ B) ∧ v = C) → (u = B → (u ⊆ v ∨ v ⊆ u)))
36	35	imp 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃y ∈ A ((B ⊆ C ∨ C ⊆ B) ∧ v = C) ∧ u = B) → (u ⊆ v ∨ v ⊆ u))
37	28, 36	sylan 457	. . . . . . . . . . . . . . . . 17 ⊢ (((∀y ∈ A (B ⊆ C ∨ C ⊆ B) ∧ ∃y ∈ A v = C) ∧ u = B) → (u ⊆ v ∨ v ⊆ u))
38	37	an32s 779	. . . . . . . . . . . . . . . 16 ⊢ (((∀y ∈ A (B ⊆ C ∨ C ⊆ B) ∧ u = B) ∧ ∃y ∈ A v = C) → (u ⊆ v ∨ v ⊆ u))
39	27, 38	sylan2b 461	. . . . . . . . . . . . . . 15 ⊢ (((∀y ∈ A (B ⊆ C ∨ C ⊆ B) ∧ u = B) ∧ v ∈ {z ∣ ∃x ∈ A z = B}) → (u ⊆ v ∨ v ⊆ u))
40	39	ralrimiva 2697	. . . . . . . . . . . . . 14 ⊢ ((∀y ∈ A (B ⊆ C ∨ C ⊆ B) ∧ u = B) → ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u))
41	40	adantll 694	. . . . . . . . . . . . 13 ⊢ (((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B) → ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u))
42	19, 41	jca 518	. . . . . . . . . . . 12 ⊢ (((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B) → ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)))
43	42	a1i 10	. . . . . . . . . . 11 ⊢ (x ∈ A → (((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B) → ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u))))
44	11, 43	rexlimi 2731	. . . . . . . . . 10 ⊢ (∃x ∈ A ((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u = B) → ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)))
45	5, 44	syl 15	. . . . . . . . 9 ⊢ ((∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ ∃x ∈ A u = B) → ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)))
46	4, 45	sylan2b 461	. . . . . . . 8 ⊢ ((∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ u ∈ {z ∣ ∃x ∈ A z = B}) → ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)))
47	46	ralrimiva 2697	. . . . . . 7 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∀u ∈ {z ∣ ∃x ∈ A z = B} ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)))
48		fun11uni 5162	. . . . . . 7 ⊢ (∀u ∈ {z ∣ ∃x ∈ A z = B} ((Fun u ∧ Fun ◡u) ∧ ∀v ∈ {z ∣ ∃x ∈ A z = B} (u ⊆ v ∨ v ⊆ u)) → (Fun ∪{z ∣ ∃x ∈ A z = B} ∧ Fun ◡∪{z ∣ ∃x ∈ A z = B}))
49	47, 48	syl 15	. . . . . 6 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (Fun ∪{z ∣ ∃x ∈ A z = B} ∧ Fun ◡∪{z ∣ ∃x ∈ A z = B}))
50	49	simpld 445	. . . . 5 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → Fun ∪{z ∣ ∃x ∈ A z = B})
51		fun11iun.2	. . . . . . 7 ⊢ B ∈ V
52	51	dfiun2 4001	. . . . . 6 ⊢ ∪x ∈ A B = ∪{z ∣ ∃x ∈ A z = B}
53	52	funeqi 5128	. . . . 5 ⊢ (Fun ∪x ∈ A B ↔ Fun ∪{z ∣ ∃x ∈ A z = B})
54	50, 53	sylibr 203	. . . 4 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → Fun ∪x ∈ A B)
55		nfra1 2664	. . . . . . 7 ⊢ Ⅎx∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B))
56		rsp 2674	. . . . . . . . 9 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (x ∈ A → (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B))))
57	56	imp 418	. . . . . . . 8 ⊢ ((∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ x ∈ A) → (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)))
58		eldm2 4899	. . . . . . . . . 10 ⊢ (u ∈ dom B ↔ ∃v⟨u, v⟩ ∈ B)
59		f1dm 5261	. . . . . . . . . . 11 ⊢ (B:D–1-1→S → dom B = D)
60	59	eleq2d 2420	. . . . . . . . . 10 ⊢ (B:D–1-1→S → (u ∈ dom B ↔ u ∈ D))
61	58, 60	syl5bbr 250	. . . . . . . . 9 ⊢ (B:D–1-1→S → (∃v⟨u, v⟩ ∈ B ↔ u ∈ D))
62	61	adantr 451	. . . . . . . 8 ⊢ ((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (∃v⟨u, v⟩ ∈ B ↔ u ∈ D))
63	57, 62	syl 15	. . . . . . 7 ⊢ ((∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) ∧ x ∈ A) → (∃v⟨u, v⟩ ∈ B ↔ u ∈ D))
64	55, 63	rexbida 2629	. . . . . 6 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (∃x ∈ A ∃v⟨u, v⟩ ∈ B ↔ ∃x ∈ A u ∈ D))
65		eliun 3973	. . . . . . . 8 ⊢ (⟨u, v⟩ ∈ ∪x ∈ A B ↔ ∃x ∈ A ⟨u, v⟩ ∈ B)
66	65	exbii 1582	. . . . . . 7 ⊢ (∃v⟨u, v⟩ ∈ ∪x ∈ A B ↔ ∃v∃x ∈ A ⟨u, v⟩ ∈ B)
67		eldm2 4899	. . . . . . 7 ⊢ (u ∈ dom ∪x ∈ A B ↔ ∃v⟨u, v⟩ ∈ ∪x ∈ A B)
68		rexcom4 2878	. . . . . . 7 ⊢ (∃x ∈ A ∃v⟨u, v⟩ ∈ B ↔ ∃v∃x ∈ A ⟨u, v⟩ ∈ B)
69	66, 67, 68	3bitr4i 268	. . . . . 6 ⊢ (u ∈ dom ∪x ∈ A B ↔ ∃x ∈ A ∃v⟨u, v⟩ ∈ B)
70		eliun 3973	. . . . . 6 ⊢ (u ∈ ∪x ∈ A D ↔ ∃x ∈ A u ∈ D)
71	64, 69, 70	3bitr4g 279	. . . . 5 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (u ∈ dom ∪x ∈ A B ↔ u ∈ ∪x ∈ A D))
72	71	eqrdv 2351	. . . 4 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → dom ∪x ∈ A B = ∪x ∈ A D)
73		df-fn 4790	. . . 4 ⊢ (∪x ∈ A B Fn ∪x ∈ A D ↔ (Fun ∪x ∈ A B ∧ dom ∪x ∈ A B = ∪x ∈ A D))
74	54, 72, 73	sylanbrc 645	. . 3 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∪x ∈ A B Fn ∪x ∈ A D)
75	65	exbii 1582	. . . . . 6 ⊢ (∃u⟨u, v⟩ ∈ ∪x ∈ A B ↔ ∃u∃x ∈ A ⟨u, v⟩ ∈ B)
76		elrn2 4897	. . . . . 6 ⊢ (v ∈ ran ∪x ∈ A B ↔ ∃u⟨u, v⟩ ∈ ∪x ∈ A B)
77		rexcom4 2878	. . . . . 6 ⊢ (∃x ∈ A ∃u⟨u, v⟩ ∈ B ↔ ∃u∃x ∈ A ⟨u, v⟩ ∈ B)
78	75, 76, 77	3bitr4i 268	. . . . 5 ⊢ (v ∈ ran ∪x ∈ A B ↔ ∃x ∈ A ∃u⟨u, v⟩ ∈ B)
79		nfv 1619	. . . . . 6 ⊢ Ⅎx v ∈ S
80		elrn2 4897	. . . . . . . . 9 ⊢ (v ∈ ran B ↔ ∃u⟨u, v⟩ ∈ B)
81		f1f 5258	. . . . . . . . . . 11 ⊢ (B:D–1-1→S → B:D–→S)
82		frn 5228	. . . . . . . . . . 11 ⊢ (B:D–→S → ran B ⊆ S)
83	81, 82	syl 15	. . . . . . . . . 10 ⊢ (B:D–1-1→S → ran B ⊆ S)
84	83	sseld 3272	. . . . . . . . 9 ⊢ (B:D–1-1→S → (v ∈ ran B → v ∈ S))
85	80, 84	syl5bir 209	. . . . . . . 8 ⊢ (B:D–1-1→S → (∃u⟨u, v⟩ ∈ B → v ∈ S))
86	85	adantr 451	. . . . . . 7 ⊢ ((B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (∃u⟨u, v⟩ ∈ B → v ∈ S))
87	56, 86	syl6 29	. . . . . 6 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (x ∈ A → (∃u⟨u, v⟩ ∈ B → v ∈ S)))
88	55, 79, 87	rexlimd 2735	. . . . 5 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (∃x ∈ A ∃u⟨u, v⟩ ∈ B → v ∈ S))
89	78, 88	syl5bi 208	. . . 4 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → (v ∈ ran ∪x ∈ A B → v ∈ S))
90	89	ssrdv 3278	. . 3 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ran ∪x ∈ A B ⊆ S)
91		df-f 4791	. . 3 ⊢ (∪x ∈ A B:∪x ∈ A D–→S ↔ (∪x ∈ A B Fn ∪x ∈ A D ∧ ran ∪x ∈ A B ⊆ S))
92	74, 90, 91	sylanbrc 645	. 2 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∪x ∈ A B:∪x ∈ A D–→S)
93	49	simprd 449	. . 3 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → Fun ◡∪{z ∣ ∃x ∈ A z = B})
94	52	cnveqi 4887	. . . 4 ⊢ ◡∪x ∈ A B = ◡∪{z ∣ ∃x ∈ A z = B}
95	94	funeqi 5128	. . 3 ⊢ (Fun ◡∪x ∈ A B ↔ Fun ◡∪{z ∣ ∃x ∈ A z = B})
96	93, 95	sylibr 203	. 2 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → Fun ◡∪x ∈ A B)
97		df-f1 4792	. 2 ⊢ (∪x ∈ A B:∪x ∈ A D–1-1→S ↔ (∪x ∈ A B:∪x ∈ A D–→S ∧ Fun ◡∪x ∈ A B))
98	92, 96, 97	sylanbrc 645	1 ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∪x ∈ A B:∪x ∈ A D–1-1→S)

Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ⊆ wss 3257  ∪cuni 3891  ∪ciun 3969  ⟨cop 4561  ^◡ccnv 4771  dom cdm 4772  ran crn 4773  Fun wfun 4775   Fn wfn 4776  –→wf 4777  –1-1→wf1 4778

This theorem was proved from 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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem 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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-swap 4724  df-co 4726  df-ima 4727  df-id 4767  df-cnv 4785  df-rn 4786  df-dm 4787  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792

This theorem is referenced by: (None)