Theorem mapunen 3397

Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255.

Hypotheses

Ref	Expression
mapunen.1	⊢ A ∈ V
mapunen.2	⊢ B ∈ V
mapunen.3	⊢ C ∈ V

Assertion

Ref	Expression
mapunen	⊢ ((A ∩ B) = ∅ → (C ↑m (A ∪ B)) ≈ ((C ↑m A) × (C ↑m B)))

Proof of Theorem mapunen

Step	Hyp	Ref	Expression
1		oprex 3018	. . 3 ⊢ (C ↑m (A ∪ B)) ∈ V
2	1	a1i 7	. 2 ⊢ ((A ∩ B) = ∅ → (C ↑m (A ∪ B)) ∈ V)
3		ssun1 1621	. . . . . . 7 ⊢ A ⊆ (A ∪ B)
4		fssres 2764	. . . . . . 7 ⊢ ((x:(A ∪ B)–→C ∧ A ⊆ (A ∪ B)) → (x ↾ A):A–→C)
5	3, 4	mpan2 519	. . . . . 6 ⊢ (x:(A ∪ B)–→C → (x ↾ A):A–→C)
6		mapunen.3	. . . . . . 7 ⊢ C ∈ V
7		mapunen.1	. . . . . . 7 ⊢ A ∈ V
8	6, 7	elmap 3265	. . . . . 6 ⊢ ((x ↾ A) ∈ (C ↑m A) ↔ (x ↾ A):A–→C)
9	5, 8	sylibr 175	. . . . 5 ⊢ (x:(A ∪ B)–→C → (x ↾ A) ∈ (C ↑m A))
10		ssun2 1622	. . . . . . 7 ⊢ B ⊆ (A ∪ B)
11		fssres 2764	. . . . . . 7 ⊢ ((x:(A ∪ B)–→C ∧ B ⊆ (A ∪ B)) → (x ↾ B):B–→C)
12	10, 11	mpan2 519	. . . . . 6 ⊢ (x:(A ∪ B)–→C → (x ↾ B):B–→C)
13		mapunen.2	. . . . . . 7 ⊢ B ∈ V
14	6, 13	elmap 3265	. . . . . 6 ⊢ ((x ↾ B) ∈ (C ↑m B) ↔ (x ↾ B):B–→C)
15	12, 14	sylibr 175	. . . . 5 ⊢ (x:(A ∪ B)–→C → (x ↾ B) ∈ (C ↑m B))
16	9, 15	jca 236	. . . 4 ⊢ (x:(A ∪ B)–→C → ((x ↾ A) ∈ (C ↑m A) ∧ (x ↾ B) ∈ (C ↑m B)))
17	7, 13	unex 1949	. . . . 5 ⊢ (A ∪ B) ∈ V
18	6, 17	elmap 3265	. . . 4 ⊢ (x ∈ (C ↑m (A ∪ B)) ↔ x:(A ∪ B)–→C)
19		visset 1350	. . . . . 6 ⊢ x ∈ V
20		resexg 2597	. . . . . 6 ⊢ (x ∈ V → (x ↾ B) ∈ V)
21	19, 20	ax-mp 6	. . . . 5 ⊢ (x ↾ B) ∈ V
22	21	opelxp 2452	. . . 4 ⊢ (⟨(x ↾ A), (x ↾ B)⟩ ∈ ((C ↑m A) × (C ↑m B)) ↔ ((x ↾ A) ∈ (C ↑m A) ∧ (x ↾ B) ∈ (C ↑m B)))
23	16, 18, 22	3imtr4 192	. . 3 ⊢ (x ∈ (C ↑m (A ∪ B)) → ⟨(x ↾ A), (x ↾ B)⟩ ∈ ((C ↑m A) × (C ↑m B)))
24	23	a1i 7	. 2 ⊢ ((A ∩ B) = ∅ → (x ∈ (C ↑m (A ∪ B)) → ⟨(x ↾ A), (x ↾ B)⟩ ∈ ((C ↑m A) × (C ↑m B))))
25		fun 2763	. . . . . 6 ⊢ (((∩∩y:A–→C ∧ ∪ran {y}:B–→C) ∧ (A ∩ B) = ∅) → (∩∩y ∪ ∪ran {y}):(A ∪ B)–→(C ∪ C))
26	6, 17	elmap 3265	. . . . . . 7 ⊢ ((∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B)) ↔ (∩∩y ∪ ∪ran {y}):(A ∪ B)–→C)
27		unidm 1603	. . . . . . . 8 ⊢ (C ∪ C) = C
28		feq3 2750	. . . . . . . 8 ⊢ ((C ∪ C) = C → ((∩∩y ∪ ∪ran {y}):(A ∪ B)–→(C ∪ C) ↔ (∩∩y ∪ ∪ran {y}):(A ∪ B)–→C))
29	27, 28	ax-mp 6	. . . . . . 7 ⊢ ((∩∩y ∪ ∪ran {y}):(A ∪ B)–→(C ∪ C) ↔ (∩∩y ∪ ∪ran {y}):(A ∪ B)–→C)
30	26, 29	bitr4 154	. . . . . 6 ⊢ ((∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B)) ↔ (∩∩y ∪ ∪ran {y}):(A ∪ B)–→(C ∪ C))
31	25, 30	sylibr 175	. . . . 5 ⊢ (((∩∩y:A–→C ∧ ∪ran {y}:B–→C) ∧ (A ∩ B) = ∅) → (∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B)))
32		elxp5 2641	. . . . . . 7 ⊢ (y ∈ ((C ↑m A) × (C ↑m B)) ↔ (y = ⟨∩∩y, ∪ran {y}⟩ ∧ (∩∩y ∈ (C ↑m A) ∧ ∪ran {y} ∈ (C ↑m B))))
33	32	pm3.27bd 263	. . . . . 6 ⊢ (y ∈ ((C ↑m A) × (C ↑m B)) → (∩∩y ∈ (C ↑m A) ∧ ∪ran {y} ∈ (C ↑m B)))
34	6, 7	elmap 3265	. . . . . . 7 ⊢ (∩∩y ∈ (C ↑m A) ↔ ∩∩y:A–→C)
35	6, 13	elmap 3265	. . . . . . 7 ⊢ (∪ran {y} ∈ (C ↑m B) ↔ ∪ran {y}:B–→C)
36	34, 35	anbi12i 369	. . . . . 6 ⊢ ((∩∩y ∈ (C ↑m A) ∧ ∪ran {y} ∈ (C ↑m B)) ↔ (∩∩y:A–→C ∧ ∪ran {y}:B–→C))
37	33, 36	sylib 173	. . . . 5 ⊢ (y ∈ ((C ↑m A) × (C ↑m B)) → (∩∩y:A–→C ∧ ∪ran {y}:B–→C))
38	31, 37	sylan 343	. . . 4 ⊢ ((y ∈ ((C ↑m A) × (C ↑m B)) ∧ (A ∩ B) = ∅) → (∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B)))
39	38	exp 291	. . 3 ⊢ (y ∈ ((C ↑m A) × (C ↑m B)) → ((A ∩ B) = ∅ → (∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B))))
40	39	com12 13	. 2 ⊢ ((A ∩ B) = ∅ → (y ∈ ((C ↑m A) × (C ↑m B)) → (∩∩y ∪ ∪ran {y}) ∈ (C ↑m (A ∪ B))))
41		opeq12 1878	. . . . . . . . . . . . . 14 ⊢ (((x ↾ A) = ∩∩y ∧ (x ↾ B) = ∪ran {y}) → ⟨(x ↾ A), (x ↾ B)⟩ = ⟨∩∩y, ∪ran {y}⟩)
42		reseq1 2575	. . . . . . . . . . . . . . . 16 ⊢ (x = (∩∩y ∪ ∪ran {y}) → (x ↾ A) = ((∩∩y ∪ ∪ran {y}) ↾ A))
43		resundir 2583	. . . . . . . . . . . . . . . 16 ⊢ ((∩∩y ∪ ∪ran {y}) ↾ A) = ((∩∩y ↾ A) ∪ (∪ran {y} ↾ A))
44	42, 43	syl6eq 1140	. . . . . . . . . . . . . . 15 ⊢ (x = (∩∩y ∪ ∪ran {y}) → (x ↾ A) = ((∩∩y ↾ A) ∪ (∪ran {y} ↾ A)))
45		fnresdm 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (∩∩y Fn A → (∩∩y ↾ A) = ∩∩y)
46	45	uneq1d 1610	. . . . . . . . . . . . . . . . 17 ⊢ (∩∩y Fn A → ((∩∩y ↾ A) ∪ (∪ran {y} ↾ A)) = (∩∩y ∪ (∪ran {y} ↾ A)))
47		fnresdisj 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ran {y} Fn B → ((B ∩ A) = ∅ ↔ (∪ran {y} ↾ A) = ∅))
48	47	biimpa 324	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∪ran {y} Fn B ∧ (B ∩ A) = ∅) → (∪ran {y} ↾ A) = ∅)
49		incom 1636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (A ∩ B) = (B ∩ A)
50	49	cleq1i 1108	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∩ B) = ∅ ↔ (B ∩ A) = ∅)
51	48, 50	sylan2b 347	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ran {y} Fn B ∧ (A ∩ B) = ∅) → (∪ran {y} ↾ A) = ∅)
52	51	uneq2d 1611	. . . . . . . . . . . . . . . . . 18 ⊢ ((∪ran {y} Fn B ∧ (A ∩ B) = ∅) → (∩∩y ∪ (∪ran {y} ↾ A)) = (∩∩y ∪ ∅))
53		un0 1721	. . . . . . . . . . . . . . . . . 18 ⊢ (∩∩y ∪ ∅) = ∩∩y
54	52, 53	syl6eq 1140	. . . . . . . . . . . . . . . . 17 ⊢ ((∪ran {y} Fn B ∧ (A ∩ B) = ∅) → (∩∩y ∪ (∪ran {y} ↾ A)) = ∩∩y)
55	46, 54	sylan9eq 1144	. . . . . . . . . . . . . . . 16 ⊢ ((∩∩y Fn A ∧ (∪ran {y} Fn B ∧ (A ∩ B) = ∅)) → ((∩∩y ↾ A) ∪ (∪ran {y} ↾ A)) = ∩∩y)
56	55	anassrs 338	. . . . . . . . . . . . . . 15 ⊢ (((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) → ((∩∩y ↾ A) ∪ (∪ran {y} ↾ A)) = ∩∩y)
57	44, 56	sylan9eqr 1145	. . . . . . . . . . . . . 14 ⊢ ((((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) ∧ x = (∩∩y ∪ ∪ran {y})) → (x ↾ A) = ∩∩y)
58		reseq1 2575	. . . . . . . . . . . . . . . 16 ⊢ (x = (∩∩y ∪ ∪ran {y}) → (x ↾ B) = ((∩∩y ∪ ∪ran {y}) ↾ B))
59		resundir 2583	. . . . . . . . . . . . . . . 16 ⊢ ((∩∩y ∪ ∪ran {y}) ↾ B) = ((∩∩y ↾ B) ∪ (∪ran {y} ↾ B))
60	58, 59	syl6eq 1140	. . . . . . . . . . . . . . 15 ⊢ (x = (∩∩y ∪ ∪ran {y}) → (x ↾ B) = ((∩∩y ↾ B) ∪ (∪ran {y} ↾ B)))
61		fnresdm 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ran {y} Fn B → (∪ran {y} ↾ B) = ∪ran {y})
62	61	uneq2d 1611	. . . . . . . . . . . . . . . . 17 ⊢ (∪ran {y} Fn B → ((∩∩y ↾ B) ∪ (∪ran {y} ↾ B)) = ((∩∩y ↾ B) ∪ ∪ran {y}))
63		fnresdisj 2732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩∩y Fn A → ((A ∩ B) = ∅ ↔ (∩∩y ↾ B) = ∅))
64	63	biimpa 324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∩∩y Fn A ∧ (A ∩ B) = ∅) → (∩∩y ↾ B) = ∅)
65	64	uneq1d 1610	. . . . . . . . . . . . . . . . . 18 ⊢ ((∩∩y Fn A ∧ (A ∩ B) = ∅) → ((∩∩y ↾ B) ∪ ∪ran {y}) = (∅ ∪ ∪ran {y}))
66		uncom 1604	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∪ ∪ran {y}) = (∪ran {y} ∪ ∅)
67		un0 1721	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ran {y} ∪ ∅) = ∪ran {y}
68	66, 67	eqtr 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∪ ∪ran {y}) = ∪ran {y}
69	65, 68	syl6eq 1140	. . . . . . . . . . . . . . . . 17 ⊢ ((∩∩y Fn A ∧ (A ∩ B) = ∅) → ((∩∩y ↾ B) ∪ ∪ran {y}) = ∪ran {y})
70	62, 69	sylan9eqr 1145	. . . . . . . . . . . . . . . 16 ⊢ (((∩∩y Fn A ∧ (A ∩ B) = ∅) ∧ ∪ran {y} Fn B) → ((∩∩y ↾ B) ∪ (∪ran {y} ↾ B)) = ∪ran {y})
71	70	an1rs 373	. . . . . . . . . . . . . . 15 ⊢ (((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) → ((∩∩y ↾ B) ∪ (∪ran {y} ↾ B)) = ∪ran {y})
72	60, 71	sylan9eqr 1145	. . . . . . . . . . . . . 14 ⊢ ((((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) ∧ x = (∩∩y ∪ ∪ran {y})) → (x ↾ B) = ∪ran {y})
73	41, 57, 72	sylanc 361	. . . . . . . . . . . . 13 ⊢ ((((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) ∧ x = (∩∩y ∪ ∪ran {y})) → ⟨(x ↾ A), (x ↾ B)⟩ = ⟨∩∩y, ∪ran {y}⟩)
74	73	cleq2d 1112	. . . . . . . . . . . 12 ⊢ ((((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) ∧ x = (∩∩y ∪ ∪ran {y})) → (y = ⟨(x ↾ A), (x ↾ B)⟩ ↔ y = ⟨∩∩y, ∪ran {y}⟩))
75	74	biimparc 327	. . . . . . . . . . 11 ⊢ ((y = ⟨∩∩y, ∪ran {y}⟩ ∧ (((∩∩y Fn A ∧ ∪ran {y} Fn B) ∧ (A ∩ B) = ∅) ∧ x = (∩∩y ∪ ∪ran {y}))) → y = ⟨(x ↾ A), (x ↾ B)⟩)
76	75	exp44 302	. . . . . . . . . 10 ⊢ (y = ⟨∩∩y, ∪ran {y}⟩ → ((∩∩y Fn A ∧ ∪ran {y} Fn B) → ((A ∩ B) = ∅ → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩))))
77	76	imp 277	. . . . . . . . 9 ⊢ ((y = ⟨∩∩y, ∪ran {y}⟩ ∧ (∩∩y Fn A ∧ ∪ran {y} Fn B)) → ((A ∩ B) = ∅ → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩)))
78		ffn 2752	. . . . . . . . . . 11 ⊢ (∩∩y:A–→C → ∩∩y Fn A)
79	34, 78	sylbi 174	. . . . . . . . . 10 ⊢ (∩∩y ∈ (C ↑m A) → ∩∩y Fn A)
80		ffn 2752	. . . . . . . . . . 11 ⊢ (∪ran {y}:B–→C → ∪ran {y} Fn B)
81	35, 80	sylbi 174	. . . . . . . . . 10 ⊢ (∪ran {y} ∈ (C ↑m B) → ∪ran {y} Fn B)
82	79, 81	anim12i 268	. . . . . . . . 9 ⊢ ((∩∩y ∈ (C ↑m A) ∧ ∪ran {y} ∈ (C ↑m B)) → (∩∩y Fn A ∧ ∪ran {y} Fn B))
83	77, 82	sylan2 346	. . . . . . . 8 ⊢ ((y = ⟨∩∩y, ∪ran {y}⟩ ∧ (∩∩y ∈ (C ↑m A) ∧ ∪ran {y} ∈ (C ↑m B))) → ((A ∩ B) = ∅ → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩)))
84	32, 83	sylbi 174	. . . . . . 7 ⊢ (y ∈ ((C ↑m A) × (C ↑m B)) → ((A ∩ B) = ∅ → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩)))
85	84	com12 13	. . . . . 6 ⊢ ((A ∩ B) = ∅ → (y ∈ ((C ↑m A) × (C ↑m B)) → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩)))
86	85	imp 277	. . . . 5 ⊢ (((A ∩ B) = ∅ ∧ y ∈ ((C ↑m A) × (C ↑m B))) → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩))
87	86	adantrl 311	. . . 4 ⊢ (((A ∩ B) = ∅ ∧ (x ∈ (C ↑m (A ∪ B)) ∧ y ∈ ((C ↑m A) × (C ↑m B)))) → (x = (∩∩y ∪ ∪ran {y}) → y = ⟨(x ↾ A), (x ↾ B)⟩))
88		ffn 2752	. . . . . . . . . 10 ⊢ (x:(A ∪ B)–→C → x Fn (A ∪ B))
89	18, 88	sylbi 174	. . . . . . . . 9 ⊢ (x ∈ (C ↑m (A ∪ B)) → x Fn (A ∪ B))
90		fnresdm 2731	. . . . . . . . 9 ⊢ (x Fn (A ∪ B) → (x ↾ (A ∪ B)) = x)
91	89, 90	syl 12	. . . . . . . 8 ⊢ (x ∈ (C ↑m (A ∪ B)) → (x ↾ (A ∪ B)) = x)
92	91	cleqcomd 1106	. . . . . . 7 ⊢ (x ∈ (C ↑m (A ∪ B)) → x = (x ↾ (A ∪ B)))
93		inteq 1968	. . . . . . . . . . 11 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ∩y = ∩⟨(x ↾ A), (x ↾ B)⟩)
94	93	inteqd 1970	. . . . . . . . . 10 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ∩∩y = ∩∩⟨(x ↾ A), (x ↾ B)⟩)
95		resexg 2597	. . . . . . . . . . . 12 ⊢ (x ∈ V → (x ↾ A) ∈ V)
96	19, 95	ax-mp 6	. . . . . . . . . . 11 ⊢ (x ↾ A) ∈ V
97	96	op1stb 1992	. . . . . . . . . 10 ⊢ ∩∩⟨(x ↾ A), (x ↾ B)⟩ = (x ↾ A)
98	94, 97	syl6eq 1140	. . . . . . . . 9 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ∩∩y = (x ↾ A))
99		sneq 1816	. . . . . . . . . . . 12 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → {y} = {⟨(x ↾ A), (x ↾ B)⟩})
100	99	rneqd 2557	. . . . . . . . . . 11 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ran {y} = ran {⟨(x ↾ A), (x ↾ B)⟩})
101	100	unieqd 1929	. . . . . . . . . 10 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ∪ran {y} = ∪ran {⟨(x ↾ A), (x ↾ B)⟩})
102	96, 21	op2nda 2639	. . . . . . . . . 10 ⊢ ∪ran {⟨(x ↾ A), (x ↾ B)⟩} = (x ↾ B)
103	101, 102	syl6eq 1140	. . . . . . . . 9 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → ∪ran {y} = (x ↾ B))
104	98, 103	uneq12d 1612	. . . . . . . 8 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → (∩∩y ∪ ∪ran {y}) = ((x ↾ A) ∪ (x ↾ B)))
105		resundi 2582	. . . . . . . 8 ⊢ (x ↾ (A ∪ B)) = ((x ↾ A) ∪ (x ↾ B))
106	104, 105	syl6reqr 1143	. . . . . . 7 ⊢ (y = ⟨(x ↾ A), (x ↾ B)⟩ → (x ↾ (A ∪ B)) = (∩∩y ∪ ∪ran {y}))
107	92, 106	sylan9eq 1144	. . . . . 6 ⊢ ((x ∈ (C ↑m (A ∪ B)) ∧ y = ⟨(x ↾ A), (x ↾ B)⟩) → x = (∩∩y ∪ ∪ran {y}))
108	107	exp 291	. . . . 5 ⊢ (x ∈ (C ↑m (A ∪ B)) → (y = ⟨(x ↾ A), (x ↾ B)⟩ → x = (∩∩y ∪ ∪ran {y})))
109	108	ad2antrl 322	. . . 4 ⊢ (((A ∩ B) = ∅ ∧ (x ∈ (C ↑m (A ∪ B)) ∧ y ∈ ((C ↑m A) × (C ↑m B)))) → (y = ⟨(x ↾ A), (x ↾ B)⟩ → x = (∩∩y ∪ ∪ran {y})))
110	87, 109	impbid 397	. . 3 ⊢ (((A ∩ B) = ∅ ∧ (x ∈ (C ↑m (A ∪ B)) ∧ y ∈ ((C ↑m A) × (C ↑m B)))) → (x = (∩∩y ∪ ∪ran {y}) ↔ y = ⟨(x ↾ A), (x ↾ B)⟩))
111	110	exp 291	. 2 ⊢ ((A ∩ B) = ∅ → ((x ∈ (C ↑m (A ∪ B)) ∧ y ∈ ((C ↑m A) × (C ↑m B))) → (x = (∩∩y ∪ ∪ran {y}) ↔ y = ⟨(x ↾ A), (x ↾ B)⟩)))
112	2, 24, 40, 111	en3d 3304	1 ⊢ ((A ∩ B) = ∅ → (C ↑m (A ∪ B)) ≈ ((C ↑m A) × (C ↑m B)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091   ∈ wcel 1092  Vcvv 1348   ∪ cun 1485   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808  ⟨cop 1810  ∪cuni 1919  ∩cint 1965   class class class wbr 2054   × cxp 2408  ran crn 2411   ↾ cres 2412   Fn wfn 2417  –→wf 2418  (class class class)co 3001   ↑_m cm 3258   ≈ cen 3271

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-int 1966  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-opr 3003  df-oprab 3004  df-map 3259  df-en 3274

metamath.org