Theorem cdaassen 3725

Description: Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258.

Hypotheses

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

Assertion

Ref	Expression
cdaassen	⊢ ((A +c B) +c C) ≈ (A +c (B +c C))

Proof of Theorem cdaassen

Step	Hyp	Ref	Expression
1		cdacomen.1	. . . . . . . . 9 ⊢ A ∈ V
2		p0ex 1885	. . . . . . . . 9 ⊢ {∅} ∈ V
3	1, 2	xpex 2488	. . . . . . . 8 ⊢ (A × {∅}) ∈ V
4		cdacomen.2	. . . . . . . . 9 ⊢ B ∈ V
5		snex 1859	. . . . . . . . 9 ⊢ {1o} ∈ V
6	4, 5	xpex 2488	. . . . . . . 8 ⊢ (B × {1o}) ∈ V
7	3, 6	unex 1949	. . . . . . 7 ⊢ ((A × {∅}) ∪ (B × {1o})) ∈ V
8	7, 2	xpex 2488	. . . . . 6 ⊢ (((A × {∅}) ∪ (B × {1o})) × {∅}) ∈ V
9		xpundir 2462	. . . . . 6 ⊢ (((A × {∅}) ∪ (B × {1o})) × {∅}) = (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅}))
10		eqeng 3296	. . . . . 6 ⊢ ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∈ V → ((((A × {∅}) ∪ (B × {1o})) × {∅}) = (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) → (((A × {∅}) ∪ (B × {1o})) × {∅}) ≈ (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅}))))
11	8, 9, 10	mp2 43	. . . . 5 ⊢ (((A × {∅}) ∪ (B × {1o})) × {∅}) ≈ (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅}))
12		cdaassen.3	. . . . . . 7 ⊢ C ∈ V
13	12, 5	xpex 2488	. . . . . 6 ⊢ (C × {1o}) ∈ V
14		1o 3109	. . . . . . . 8 ⊢ 1o ∈ On
15	14	elisseti 1355	. . . . . . 7 ⊢ 1o ∈ V
16	13, 15	xpsnen 3339	. . . . . 6 ⊢ ((C × {1o}) × {1o}) ≈ (C × {1o})
17	13, 16	ensymi 3318	. . . . 5 ⊢ (C × {1o}) ≈ ((C × {1o}) × {1o})
18	11, 17	pm3.2i 234	. . . 4 ⊢ ((((A × {∅}) ∪ (B × {1o})) × {∅}) ≈ (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∧ (C × {1o}) ≈ ((C × {1o}) × {1o}))
19		0ne1oOLD 3113	. . . . . 6 ⊢ ¬ ∅ = 1o
20		xpsndisj 2655	. . . . . 6 ⊢ (¬ ∅ = 1o → ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∩ (C × {1o})) = ∅)
21	19, 20	ax-mp 6	. . . . 5 ⊢ ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∩ (C × {1o})) = ∅
22		xpsndisj 2655	. . . . . . . 8 ⊢ (¬ ∅ = 1o → (((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅)
23	19, 22	ax-mp 6	. . . . . . 7 ⊢ (((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅
24		xpsndisj 2655	. . . . . . . 8 ⊢ (¬ ∅ = 1o → (((B × {1o}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅)
25	19, 24	ax-mp 6	. . . . . . 7 ⊢ (((B × {1o}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅
26	23, 25	pm3.2i 234	. . . . . 6 ⊢ ((((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅ ∧ (((B × {1o}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅)
27		undisj1 1739	. . . . . 6 ⊢ (((((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅ ∧ (((B × {1o}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅) ↔ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅)
28	26, 27	mpbi 164	. . . . 5 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅
29	21, 28	pm3.2i 234	. . . 4 ⊢ (((((A × {∅}) ∪ (B × {1o})) × {∅}) ∩ (C × {1o})) = ∅ ∧ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅)
30		unen 3338	. . . 4 ⊢ ((((((A × {∅}) ∪ (B × {1o})) × {∅}) ≈ (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∧ (C × {1o}) ≈ ((C × {1o}) × {1o})) ∧ (((((A × {∅}) ∪ (B × {1o})) × {∅}) ∩ (C × {1o})) = ∅ ∧ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅)) → ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∪ (C × {1o})) ≈ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o})))
31	18, 29, 30	mp2an 520	. . 3 ⊢ ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∪ (C × {1o})) ≈ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o}))
32	3, 2	xpex 2488	. . . . 5 ⊢ ((A × {∅}) × {∅}) ∈ V
33	4, 2	xpex 2488	. . . . . . 7 ⊢ (B × {∅}) ∈ V
34	33, 5	xpex 2488	. . . . . 6 ⊢ ((B × {∅}) × {1o}) ∈ V
35	13, 5	xpex 2488	. . . . . 6 ⊢ ((C × {1o}) × {1o}) ∈ V
36	34, 35	unex 1949	. . . . 5 ⊢ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})) ∈ V
37	32, 36	unex 1949	. . . 4 ⊢ (((A × {∅}) × {∅}) ∪ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) ∈ V
38	32	enref 3295	. . . . . . . . 9 ⊢ ((A × {∅}) × {∅}) ≈ ((A × {∅}) × {∅})
39	4, 5, 2	xpassen 3344	. . . . . . . . . 10 ⊢ ((B × {1o}) × {∅}) ≈ (B × ({1o} × {∅}))
40	2, 5	xpex 2488	. . . . . . . . . . . 12 ⊢ ({∅} × {1o}) ∈ V
41	4, 40	xpex 2488	. . . . . . . . . . 11 ⊢ (B × ({∅} × {1o})) ∈ V
42	4	enref 3295	. . . . . . . . . . . 12 ⊢ B ≈ B
43	5, 2	xpcomen 3343	. . . . . . . . . . . 12 ⊢ ({1o} × {∅}) ≈ ({∅} × {1o})
44	5, 2	xpex 2488	. . . . . . . . . . . . 13 ⊢ ({1o} × {∅}) ∈ V
45	4, 4, 44, 40	xpen 3383	. . . . . . . . . . . 12 ⊢ ((B ≈ B ∧ ({1o} × {∅}) ≈ ({∅} × {1o})) → (B × ({1o} × {∅})) ≈ (B × ({∅} × {1o})))
46	42, 43, 45	mp2an 520	. . . . . . . . . . 11 ⊢ (B × ({1o} × {∅})) ≈ (B × ({∅} × {1o}))
47	4, 2, 5	xpassen 3344	. . . . . . . . . . 11 ⊢ ((B × {∅}) × {1o}) ≈ (B × ({∅} × {1o}))
48	41, 46, 47	entr4 3324	. . . . . . . . . 10 ⊢ (B × ({1o} × {∅})) ≈ ((B × {∅}) × {1o})
49	39, 48	entr 3321	. . . . . . . . 9 ⊢ ((B × {1o}) × {∅}) ≈ ((B × {∅}) × {1o})
50	38, 49	pm3.2i 234	. . . . . . . 8 ⊢ (((A × {∅}) × {∅}) ≈ ((A × {∅}) × {∅}) ∧ ((B × {1o}) × {∅}) ≈ ((B × {∅}) × {1o}))
51		xpsndisj 2655	. . . . . . . . . . . 12 ⊢ (¬ ∅ = 1o → ((A × {∅}) ∩ (B × {1o})) = ∅)
52	19, 51	ax-mp 6	. . . . . . . . . . 11 ⊢ ((A × {∅}) ∩ (B × {1o})) = ∅
53		xpeq1 2440	. . . . . . . . . . 11 ⊢ (((A × {∅}) ∩ (B × {1o})) = ∅ → (((A × {∅}) ∩ (B × {1o})) × {∅}) = (∅ × {∅}))
54	52, 53	ax-mp 6	. . . . . . . . . 10 ⊢ (((A × {∅}) ∩ (B × {1o})) × {∅}) = (∅ × {∅})
55		xpindir 2498	. . . . . . . . . 10 ⊢ (((A × {∅}) ∩ (B × {1o})) × {∅}) = (((A × {∅}) × {∅}) ∩ ((B × {1o}) × {∅}))
56		xp0r 2474	. . . . . . . . . 10 ⊢ (∅ × {∅}) = ∅
57	54, 55, 56	3eqtr3 1124	. . . . . . . . 9 ⊢ (((A × {∅}) × {∅}) ∩ ((B × {1o}) × {∅})) = ∅
58		xpsndisj 2655	. . . . . . . . . 10 ⊢ (¬ ∅ = 1o → (((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅)
59	19, 58	ax-mp 6	. . . . . . . . 9 ⊢ (((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅
60	57, 59	pm3.2i 234	. . . . . . . 8 ⊢ ((((A × {∅}) × {∅}) ∩ ((B × {1o}) × {∅})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅)
61		unen 3338	. . . . . . . 8 ⊢ (((((A × {∅}) × {∅}) ≈ ((A × {∅}) × {∅}) ∧ ((B × {1o}) × {∅}) ≈ ((B × {∅}) × {1o})) ∧ ((((A × {∅}) × {∅}) ∩ ((B × {1o}) × {∅})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅)) → (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ≈ (((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})))
62	50, 60, 61	mp2an 520	. . . . . . 7 ⊢ (((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ≈ (((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o}))
63	35	enref 3295	. . . . . . 7 ⊢ ((C × {1o}) × {1o}) ≈ ((C × {1o}) × {1o})
64	62, 63	pm3.2i 234	. . . . . 6 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ≈ (((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∧ ((C × {1o}) × {1o}) ≈ ((C × {1o}) × {1o}))
65		xpsndisj 2655	. . . . . . . . . . . 12 ⊢ (¬ ∅ = 1o → ((B × {∅}) ∩ (C × {1o})) = ∅)
66	19, 65	ax-mp 6	. . . . . . . . . . 11 ⊢ ((B × {∅}) ∩ (C × {1o})) = ∅
67		xpeq1 2440	. . . . . . . . . . 11 ⊢ (((B × {∅}) ∩ (C × {1o})) = ∅ → (((B × {∅}) ∩ (C × {1o})) × {1o}) = (∅ × {1o}))
68	66, 67	ax-mp 6	. . . . . . . . . 10 ⊢ (((B × {∅}) ∩ (C × {1o})) × {1o}) = (∅ × {1o})
69		xpindir 2498	. . . . . . . . . 10 ⊢ (((B × {∅}) ∩ (C × {1o})) × {1o}) = (((B × {∅}) × {1o}) ∩ ((C × {1o}) × {1o}))
70		xp0r 2474	. . . . . . . . . 10 ⊢ (∅ × {1o}) = ∅
71	68, 69, 70	3eqtr3 1124	. . . . . . . . 9 ⊢ (((B × {∅}) × {1o}) ∩ ((C × {1o}) × {1o})) = ∅
72	23, 71	pm3.2i 234	. . . . . . . 8 ⊢ ((((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅ ∧ (((B × {∅}) × {1o}) ∩ ((C × {1o}) × {1o})) = ∅)
73		undisj1 1739	. . . . . . . 8 ⊢ (((((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅ ∧ (((B × {∅}) × {1o}) ∩ ((C × {1o}) × {1o})) = ∅) ↔ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∩ ((C × {1o}) × {1o})) = ∅)
74	72, 73	mpbi 164	. . . . . . 7 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∩ ((C × {1o}) × {1o})) = ∅
75	28, 74	pm3.2i 234	. . . . . 6 ⊢ (((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅ ∧ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∩ ((C × {1o}) × {1o})) = ∅)
76		unen 3338	. . . . . 6 ⊢ ((((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ≈ (((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∧ ((C × {1o}) × {1o}) ≈ ((C × {1o}) × {1o})) ∧ (((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∩ ((C × {1o}) × {1o})) = ∅ ∧ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∩ ((C × {1o}) × {1o})) = ∅)) → ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o})) ≈ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∪ ((C × {1o}) × {1o})))
77	64, 75, 76	mp2an 520	. . . . 5 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o})) ≈ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∪ ((C × {1o}) × {1o}))
78		unass 1615	. . . . 5 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {∅}) × {1o})) ∪ ((C × {1o}) × {1o})) = (((A × {∅}) × {∅}) ∪ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})))
79	77, 78	breqtr 2080	. . . 4 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o})) ≈ (((A × {∅}) × {∅}) ∪ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})))
80		0ex 1745	. . . . . . . 8 ⊢ ∅ ∈ V
81	3, 80	xpsnen 3339	. . . . . . 7 ⊢ ((A × {∅}) × {∅}) ≈ (A × {∅})
82	3, 81	ensymi 3318	. . . . . 6 ⊢ (A × {∅}) ≈ ((A × {∅}) × {∅})
83	33, 13	unex 1949	. . . . . . . 8 ⊢ ((B × {∅}) ∪ (C × {1o})) ∈ V
84	83, 5	xpex 2488	. . . . . . 7 ⊢ (((B × {∅}) ∪ (C × {1o})) × {1o}) ∈ V
85		xpundir 2462	. . . . . . 7 ⊢ (((B × {∅}) ∪ (C × {1o})) × {1o}) = (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))
86		eqeng 3296	. . . . . . 7 ⊢ ((((B × {∅}) ∪ (C × {1o})) × {1o}) ∈ V → ((((B × {∅}) ∪ (C × {1o})) × {1o}) = (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})) → (((B × {∅}) ∪ (C × {1o})) × {1o}) ≈ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))))
87	84, 85, 86	mp2 43	. . . . . 6 ⊢ (((B × {∅}) ∪ (C × {1o})) × {1o}) ≈ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))
88	82, 87	pm3.2i 234	. . . . 5 ⊢ ((A × {∅}) ≈ ((A × {∅}) × {∅}) ∧ (((B × {∅}) ∪ (C × {1o})) × {1o}) ≈ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})))
89		xpsndisj 2655	. . . . . . 7 ⊢ (¬ ∅ = 1o → ((A × {∅}) ∩ (((B × {∅}) ∪ (C × {1o})) × {1o})) = ∅)
90	19, 89	ax-mp 6	. . . . . 6 ⊢ ((A × {∅}) ∩ (((B × {∅}) ∪ (C × {1o})) × {1o})) = ∅
91	59, 23	pm3.2i 234	. . . . . . 7 ⊢ ((((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅)
92		undisj2 1740	. . . . . . 7 ⊢ (((((A × {∅}) × {∅}) ∩ ((B × {∅}) × {1o})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ ((C × {1o}) × {1o})) = ∅) ↔ (((A × {∅}) × {∅}) ∩ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) = ∅)
93	91, 92	mpbi 164	. . . . . 6 ⊢ (((A × {∅}) × {∅}) ∩ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) = ∅
94	90, 93	pm3.2i 234	. . . . 5 ⊢ (((A × {∅}) ∩ (((B × {∅}) ∪ (C × {1o})) × {1o})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) = ∅)
95		unen 3338	. . . . 5 ⊢ ((((A × {∅}) ≈ ((A × {∅}) × {∅}) ∧ (((B × {∅}) ∪ (C × {1o})) × {1o}) ≈ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) ∧ (((A × {∅}) ∩ (((B × {∅}) ∪ (C × {1o})) × {1o})) = ∅ ∧ (((A × {∅}) × {∅}) ∩ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))) = ∅)) → ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o})) ≈ (((A × {∅}) × {∅}) ∪ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o}))))
96	88, 94, 95	mp2an 520	. . . 4 ⊢ ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o})) ≈ (((A × {∅}) × {∅}) ∪ (((B × {∅}) × {1o}) ∪ ((C × {1o}) × {1o})))
97	37, 79, 96	entr4 3324	. . 3 ⊢ ((((A × {∅}) × {∅}) ∪ ((B × {1o}) × {∅})) ∪ ((C × {1o}) × {1o})) ≈ ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o}))
98	31, 97	entr 3321	. 2 ⊢ ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∪ (C × {1o})) ≈ ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o}))
99	1, 4	cdaval 3717	. . . 4 ⊢ (A +c B) = ((A × {∅}) ∪ (B × {1o}))
100	99	opreq1i 3009	. . 3 ⊢ ((A +c B) +c C) = (((A × {∅}) ∪ (B × {1o})) +c C)
101	7, 12	cdaval 3717	. . 3 ⊢ (((A × {∅}) ∪ (B × {1o})) +c C) = ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∪ (C × {1o}))
102	100, 101	eqtr 1119	. 2 ⊢ ((A +c B) +c C) = ((((A × {∅}) ∪ (B × {1o})) × {∅}) ∪ (C × {1o}))
103	4, 12	cdaval 3717	. . . 4 ⊢ (B +c C) = ((B × {∅}) ∪ (C × {1o}))
104	103	opreq2i 3010	. . 3 ⊢ (A +c (B +c C)) = (A +c ((B × {∅}) ∪ (C × {1o})))
105	1, 83	cdaval 3717	. . 3 ⊢ (A +c ((B × {∅}) ∪ (C × {1o}))) = ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o}))
106	104, 105	eqtr 1119	. 2 ⊢ (A +c (B +c C)) = ((A × {∅}) ∪ (((B × {∅}) ∪ (C × {1o})) × {1o}))
107	98, 102, 106	3brtr4 2085	1 ⊢ ((A +c B) +c C) ≈ (A +c (B +c C))

Syntax hints:  ¬ wn 1   ∧ wa 196   = wceq 1091   ∈ wcel 1092  Vcvv 1348   ∪ cun 1485   ∩ cin 1486  ∅c0 1707  {csn 1808   class class class wbr 2054  Oncon0 2199   × cxp 2408  (class class class)co 3001  1_oc1o 3099   ≈ cen 3271   +_c ccda 3714

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-3or 582  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-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-suc 2205  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-1o 3104  df-er 3200  df-en 3274  df-dom 3275  df-cda 3715

metamath.org