Theorem unidom 4818

Description: An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98.

Hypotheses

Ref	Expression
unidom.1	⊢ A ∈ V
unidom.2	⊢ B ∈ V

Assertion

Ref	Expression
unidom	⊢ (∀x ∈ A x ≼ B → ∪A ≼ (A × B))

Distinct variable groups:   x,A   x,B

Proof of Theorem unidom

Step	Hyp	Ref	Expression
1		unidom.1	. . . . . . 7 ⊢ A ∈ V
2	1	uniex 2876	. . . . . 6 ⊢ ∪A ∈ V
3		id 59	. . . . . . . . . . . . . 14 ⊢ (x = y → x = y)
4		fveq2 3730	. . . . . . . . . . . . . 14 ⊢ (x = y → (h ‘x) = (h ‘y))
5	3, 4	eleq12d 1545	. . . . . . . . . . . . 13 ⊢ (x = y → (x ∈ (h ‘x) ↔ y ∈ (h ‘y)))
6	4	eleq1d 1543	. . . . . . . . . . . . 13 ⊢ (x = y → ((h ‘x) ∈ A ↔ (h ‘y) ∈ A))
7	5, 6	anbi12d 630	. . . . . . . . . . . 12 ⊢ (x = y → ((x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ↔ (y ∈ (h ‘y) ⋀ (h ‘y) ∈ A)))
8	7	rcla4cv 1877	. . . . . . . . . . 11 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → (y ∈ (h ‘y) ⋀ (h ‘y) ∈ A)))
9		pm3.27 323	. . . . . . . . . . 11 ⊢ ((y ∈ (h ‘y) ⋀ (h ‘y) ∈ A) → (h ‘y) ∈ A)
10	8, 9	syl6 22	. . . . . . . . . 10 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → (h ‘y) ∈ A))
11	10	adantl 390	. . . . . . . . 9 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → (y ∈ ∪A → (h ‘y) ∈ A))
12		fveq2 3730	. . . . . . . . . . . . . . . . 17 ⊢ (x = (h ‘y) → (f ‘x) = (f ‘(h ‘y)))
13		f1eq1 3666	. . . . . . . . . . . . . . . . 17 ⊢ ((f ‘x) = (f ‘(h ‘y)) → ((f ‘x):x–1-1→B ↔ (f ‘(h ‘y)):x–1-1→B))
14	12, 13	syl 10	. . . . . . . . . . . . . . . 16 ⊢ (x = (h ‘y) → ((f ‘x):x–1-1→B ↔ (f ‘(h ‘y)):x–1-1→B))
15		f1eq2 3667	. . . . . . . . . . . . . . . 16 ⊢ (x = (h ‘y) → ((f ‘(h ‘y)):x–1-1→B ↔ (f ‘(h ‘y)):(h ‘y)–1-1→B))
16	14, 15	bitrd 530	. . . . . . . . . . . . . . 15 ⊢ (x = (h ‘y) → ((f ‘x):x–1-1→B ↔ (f ‘(h ‘y)):(h ‘y)–1-1→B))
17	16	rcla4v 1876	. . . . . . . . . . . . . 14 ⊢ ((h ‘y) ∈ A → (∀x ∈ A (f ‘x):x–1-1→B → (f ‘(h ‘y)):(h ‘y)–1-1→B))
18		f1f 3671	. . . . . . . . . . . . . 14 ⊢ ((f ‘(h ‘y)):(h ‘y)–1-1→B → (f ‘(h ‘y)):(h ‘y)–→B)
19	17, 18	syl6 22	. . . . . . . . . . . . 13 ⊢ ((h ‘y) ∈ A → (∀x ∈ A (f ‘x):x–1-1→B → (f ‘(h ‘y)):(h ‘y)–→B))
20		ffvelrn 3820	. . . . . . . . . . . . . 14 ⊢ (((f ‘(h ‘y)):(h ‘y)–→B ⋀ y ∈ (h ‘y)) → ((f ‘(h ‘y)) ‘y) ∈ B)
21	20	expcom 374	. . . . . . . . . . . . 13 ⊢ (y ∈ (h ‘y) → ((f ‘(h ‘y)):(h ‘y)–→B → ((f ‘(h ‘y)) ‘y) ∈ B))
22	19, 21	sylan9r 471	. . . . . . . . . . . 12 ⊢ ((y ∈ (h ‘y) ⋀ (h ‘y) ∈ A) → (∀x ∈ A (f ‘x):x–1-1→B → ((f ‘(h ‘y)) ‘y) ∈ B))
23	8, 22	syl6 22	. . . . . . . . . . 11 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → (∀x ∈ A (f ‘x):x–1-1→B → ((f ‘(h ‘y)) ‘y) ∈ B)))
24	23	com3r 35	. . . . . . . . . 10 ⊢ (∀x ∈ A (f ‘x):x–1-1→B → (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → ((f ‘(h ‘y)) ‘y) ∈ B)))
25	24	imp 350	. . . . . . . . 9 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → (y ∈ ∪A → ((f ‘(h ‘y)) ‘y) ∈ B))
26	11, 25	jcad 602	. . . . . . . 8 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → (y ∈ ∪A → ((h ‘y) ∈ A ⋀ ((f ‘(h ‘y)) ‘y) ∈ B)))
27		opelxpi 3223	. . . . . . . 8 ⊢ (((h ‘y) ∈ A ⋀ ((f ‘(h ‘y)) ‘y) ∈ B) → ⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ ∈ (A × B))
28	26, 27	syl6 22	. . . . . . 7 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → (y ∈ ∪A → ⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ ∈ (A × B)))
29		fveq2 3730	. . . . . . . . . . . . . . 15 ⊢ ((h ‘y) = (h ‘z) → (f ‘(h ‘y)) = (f ‘(h ‘z)))
30	29	fveq1d 3732	. . . . . . . . . . . . . 14 ⊢ ((h ‘y) = (h ‘z) → ((f ‘(h ‘y)) ‘z) = ((f ‘(h ‘z)) ‘z))
31	30	eqeq2d 1489	. . . . . . . . . . . . 13 ⊢ ((h ‘y) = (h ‘z) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘y)) ‘z) ↔ ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z)))
32	31	adantl 390	. . . . . . . . . . . 12 ⊢ ((((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘y)) ‘z) ↔ ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z)))
33		f1fveq 3882	. . . . . . . . . . . . . 14 ⊢ (((f ‘(h ‘y)):(h ‘y)–1-1→B ⋀ (y ∈ (h ‘y) ⋀ z ∈ (h ‘y))) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘y)) ‘z) ↔ y = z))
34	33	biimpd 153	. . . . . . . . . . . . 13 ⊢ (((f ‘(h ‘y)):(h ‘y)–1-1→B ⋀ (y ∈ (h ‘y) ⋀ z ∈ (h ‘y))) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘y)) ‘z) → y = z))
35	17	adantl 390	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ (h ‘y) ⋀ (h ‘y) ∈ A) → (∀x ∈ A (f ‘x):x–1-1→B → (f ‘(h ‘y)):(h ‘y)–1-1→B))
36	8, 35	syl6 22	. . . . . . . . . . . . . . . . 17 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → (∀x ∈ A (f ‘x):x–1-1→B → (f ‘(h ‘y)):(h ‘y)–1-1→B)))
37	36	com3r 35	. . . . . . . . . . . . . . . 16 ⊢ (∀x ∈ A (f ‘x):x–1-1→B → (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → (f ‘(h ‘y)):(h ‘y)–1-1→B)))
38	37	imp31 362	. . . . . . . . . . . . . . 15 ⊢ (((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ y ∈ ∪A) → (f ‘(h ‘y)):(h ‘y)–1-1→B)
39	38	adantrr 397	. . . . . . . . . . . . . 14 ⊢ (((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) → (f ‘(h ‘y)):(h ‘y)–1-1→B)
40	39	adantr 391	. . . . . . . . . . . . 13 ⊢ ((((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (f ‘(h ‘y)):(h ‘y)–1-1→B)
41		pm3.26 319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ (h ‘y) ⋀ (h ‘y) ∈ A) → y ∈ (h ‘y))
42	8, 41	syl6 22	. . . . . . . . . . . . . . . . . 18 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (y ∈ ∪A → y ∈ (h ‘y)))
43	42	adantr 391	. . . . . . . . . . . . . . . . 17 ⊢ ((∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ⋀ (h ‘y) = (h ‘z)) → (y ∈ ∪A → y ∈ (h ‘y)))
44		id 59	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = z → x = z)
45		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = z → (h ‘x) = (h ‘z))
46	44, 45	eleq12d 1545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = z → (x ∈ (h ‘x) ↔ z ∈ (h ‘z)))
47	45	eleq1d 1543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = z → ((h ‘x) ∈ A ↔ (h ‘z) ∈ A))
48	46, 47	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = z → ((x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ↔ (z ∈ (h ‘z) ⋀ (h ‘z) ∈ A)))
49	48	rcla4cv 1877	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (z ∈ ∪A → (z ∈ (h ‘z) ⋀ (h ‘z) ∈ A)))
50		pm3.26 319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ (h ‘z) ⋀ (h ‘z) ∈ A) → z ∈ (h ‘z))
51	49, 50	syl6 22	. . . . . . . . . . . . . . . . . 18 ⊢ (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → (z ∈ ∪A → z ∈ (h ‘z)))
52		eleq2 1538	. . . . . . . . . . . . . . . . . . 19 ⊢ ((h ‘y) = (h ‘z) → (z ∈ (h ‘y) ↔ z ∈ (h ‘z)))
53	52	biimprd 154	. . . . . . . . . . . . . . . . . 18 ⊢ ((h ‘y) = (h ‘z) → (z ∈ (h ‘z) → z ∈ (h ‘y)))
54	51, 53	sylan9 470	. . . . . . . . . . . . . . . . 17 ⊢ ((∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ⋀ (h ‘y) = (h ‘z)) → (z ∈ ∪A → z ∈ (h ‘y)))
55	43, 54	anim12d 560	. . . . . . . . . . . . . . . 16 ⊢ ((∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ⋀ (h ‘y) = (h ‘z)) → ((y ∈ ∪A ⋀ z ∈ ∪A) → (y ∈ (h ‘y) ⋀ z ∈ (h ‘y))))
56	55	imp 350	. . . . . . . . . . . . . . 15 ⊢ (((∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ⋀ (h ‘y) = (h ‘z)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) → (y ∈ (h ‘y) ⋀ z ∈ (h ‘y)))
57	56	an1rs 491	. . . . . . . . . . . . . 14 ⊢ (((∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (y ∈ (h ‘y) ⋀ z ∈ (h ‘y)))
58	57	adantlll 398	. . . . . . . . . . . . 13 ⊢ ((((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (y ∈ (h ‘y) ⋀ z ∈ (h ‘y)))
59	34, 40, 58	sylanc 473	. . . . . . . . . . . 12 ⊢ ((((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘y)) ‘z) → y = z))
60	32, 59	sylbird 205	. . . . . . . . . . 11 ⊢ ((((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) ⋀ (h ‘y) = (h ‘z)) → (((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z) → y = z))
61	60	expimpd 375	. . . . . . . . . 10 ⊢ (((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) → (((h ‘y) = (h ‘z) ⋀ ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z)) → y = z))
62		fvex 3738	. . . . . . . . . . 11 ⊢ (h ‘y) ∈ V
63		fvex 3738	. . . . . . . . . . 11 ⊢ ((f ‘(h ‘y)) ‘y) ∈ V
64		fvex 3738	. . . . . . . . . . 11 ⊢ ((f ‘(h ‘z)) ‘z) ∈ V
65	62, 63, 64	opth 2793	. . . . . . . . . 10 ⊢ (⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ = ⟨(h ‘z), ((f ‘(h ‘z)) ‘z)⟩ ↔ ((h ‘y) = (h ‘z) ⋀ ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z)))
66	61, 65	syl5ib 206	. . . . . . . . 9 ⊢ (((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) → (⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ = ⟨(h ‘z), ((f ‘(h ‘z)) ‘z)⟩ → y = z))
67		fveq2 3730	. . . . . . . . . 10 ⊢ (y = z → (h ‘y) = (h ‘z))
68	67	fveq2d 3734	. . . . . . . . . . . 12 ⊢ (y = z → (f ‘(h ‘y)) = (f ‘(h ‘z)))
69	68	fveq1d 3732	. . . . . . . . . . 11 ⊢ (y = z → ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘y))
70		fveq2 3730	. . . . . . . . . . 11 ⊢ (y = z → ((f ‘(h ‘z)) ‘y) = ((f ‘(h ‘z)) ‘z))
71	69, 70	eqtrd 1510	. . . . . . . . . 10 ⊢ (y = z → ((f ‘(h ‘y)) ‘y) = ((f ‘(h ‘z)) ‘z))
72	67, 71	opeq12d 2499	. . . . . . . . 9 ⊢ (y = z → ⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ = ⟨(h ‘z), ((f ‘(h ‘z)) ‘z)⟩)
73	66, 72	impbid1 519	. . . . . . . 8 ⊢ (((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) ⋀ (y ∈ ∪A ⋀ z ∈ ∪A)) → (⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ = ⟨(h ‘z), ((f ‘(h ‘z)) ‘z)⟩ ↔ y = z))
74	73	ex 373	. . . . . . 7 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → ((y ∈ ∪A ⋀ z ∈ ∪A) → (⟨(h ‘y), ((f ‘(h ‘y)) ‘y)⟩ = ⟨(h ‘z), ((f ‘(h ‘z)) ‘z)⟩ ↔ y = z)))
75	28, 74	dom2d 4410	. . . . . 6 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → (∪A ∈ V → ∪A ≼ (A × B)))
76	2, 75	mpi 44	. . . . 5 ⊢ ((∀x ∈ A (f ‘x):x–1-1→B ⋀ ∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)) → ∪A ≼ (A × B))
77	76	ex 373	. . . 4 ⊢ (∀x ∈ A (f ‘x):x–1-1→B → (∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → ∪A ≼ (A × B)))
78	77	19.23adv 1216	. . 3 ⊢ (∀x ∈ A (f ‘x):x–1-1→B → (∃h∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → ∪A ≼ (A × B)))
79	78	19.23aiv 1297	. 2 ⊢ (∃f∀x ∈ A (f ‘x):x–1-1→B → (∃h∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A) → ∪A ≼ (A × B)))
80		unidom.2	. . . . 5 ⊢ B ∈ V
81	80	brdom 4384	. . . 4 ⊢ (x ≼ B ↔ ∃g g:x–1-1→B)
82	81	ralbii 1670	. . 3 ⊢ (∀x ∈ A x ≼ B ↔ ∀x ∈ A ∃g g:x–1-1→B)
83		f1eq1 3666	. . . 4 ⊢ (g = (f ‘x) → (g:x–1-1→B ↔ (f ‘x):x–1-1→B))
84	1, 83	ac6s3 4769	. . 3 ⊢ (∀x ∈ A ∃g g:x–1-1→B → ∃f∀x ∈ A (f ‘x):x–1-1→B)
85	82, 84	sylbi 199	. 2 ⊢ (∀x ∈ A x ≼ B → ∃f∀x ∈ A (f ‘x):x–1-1→B)
86		eleq2 1538	. . . . . 6 ⊢ (g = (h ‘x) → (x ∈ g ↔ x ∈ (h ‘x)))
87		eleq1 1537	. . . . . 6 ⊢ (g = (h ‘x) → (g ∈ A ↔ (h ‘x) ∈ A))
88	86, 87	anbi12d 630	. . . . 5 ⊢ (g = (h ‘x) → ((x ∈ g ⋀ g ∈ A) ↔ (x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)))
89	2, 88	ac6s3 4769	. . . 4 ⊢ (∀x ∈ ∪A∃g(x ∈ g ⋀ g ∈ A) → ∃h∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A))
90		eluni 2510	. . . . 5 ⊢ (x ∈ ∪A ↔ ∃g(x ∈ g ⋀ g ∈ A))
91	90	biimp 151	. . . 4 ⊢ (x ∈ ∪A → ∃g(x ∈ g ⋀ g ∈ A))
92	89, 91	mprg 1703	. . 3 ⊢ ∃h∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A)
93	92	a1i 8	. 2 ⊢ (∀x ∈ A x ≼ B → ∃h∀x ∈ ∪A(x ∈ (h ‘x) ⋀ (h ‘x) ∈ A))
94	79, 85, 93	sylc 68	1 ⊢ (∀x ∈ A x ≼ B → ∪A ≼ (A × B))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∃wex 982  ∀wral 1648  Vcvv 1814  ⟨cop 2415  ∪cuni 2507   class class class wbr 2624   × cxp 3174  –→wf 3184  –1-1→wf1 3185   ‘cfv 3188   ≼ cdom 4371

This theorem is referenced by:  unidomg 4819

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-reg 4602  ax-inf2 4634  ax-ac 4754

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-iin 2573  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-rdg 3938  df-en 4374  df-dom 4375  df-r1 4653  df-rank 4654

Copyright terms: Public domain