Theorem brwdom2 9580

Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)

Assertion

Ref	Expression
brwdom2	⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))

Distinct variable groups:   𝑦,𝑋,𝑧   𝑦,𝑌,𝑧

Allowed substitution hints:   𝑉(𝑦, 𝑧)

Proof of Theorem brwdom2

Dummy variables 𝑥 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3475	. 2 ⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ V)
2		0wdom 9577	. . . . . 6 ⊢ (𝑌 ∈ V → ∅ ≼* 𝑌)
3		breq1 5109	. . . . . 6 ⊢ (𝑋 = ∅ → (𝑋 ≼* 𝑌 ↔ ∅ ≼* 𝑌))
4	2, 3	syl5ibrcom 250	. . . . 5 ⊢ (𝑌 ∈ V → (𝑋 = ∅ → 𝑋 ≼* 𝑌))
5	4	imp 412	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → 𝑋 ≼* 𝑌)
6		0elpw 5321	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑌
7		f1o0 6873	. . . . . . . 8 ⊢ ∅:∅–1-1-onto→∅
8		f1ofo 6843	. . . . . . . 8 ⊢ (∅:∅–1-1-onto→∅ → ∅:∅–onto→∅)
9		0ex 5264	. . . . . . . . 9 ⊢ ∅ ∈ V
10		foeq1 6803	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (𝑧:∅–onto→∅ ↔ ∅:∅–onto→∅))
11	9, 10	spcev 3564	. . . . . . . 8 ⊢ (∅:∅–onto→∅ → ∃𝑧 𝑧:∅–onto→∅)
12	7, 8, 11	mp2b 10	. . . . . . 7 ⊢ ∃𝑧 𝑧:∅–onto→∅
13		foeq2 6804	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑧:𝑦–onto→∅ ↔ 𝑧:∅–onto→∅))
14	13	exbidv 1955	. . . . . . . 8 ⊢ (𝑦 = ∅ → (∃𝑧 𝑧:𝑦–onto→∅ ↔ ∃𝑧 𝑧:∅–onto→∅))
15	14	rspcev 3580	. . . . . . 7 ⊢ ((∅ ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:∅–onto→∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅)
16	6, 12, 15	mp2an 705	. . . . . 6 ⊢ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅
17		foeq3 6805	. . . . . . . 8 ⊢ (𝑋 = ∅ → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑦–onto→∅))
18	17	exbidv 1955	. . . . . . 7 ⊢ (𝑋 = ∅ → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑦–onto→∅))
19	18	rexbidv 3190	. . . . . 6 ⊢ (𝑋 = ∅ → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅))
20	16, 19	mpbiri 261	. . . . 5 ⊢ (𝑋 = ∅ → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
21	20	adantl 487	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
22	5, 21	2thd 268	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
23		brwdomn0 9576	. . . . 5 ⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
24	23	adantl 487	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
25		foeq1 6803	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥:𝑌–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
26	25	cbvexvw 2071	. . . . . 6 ⊢ (∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)
27		pwidg 4581	. . . . . . . . 9 ⊢ (𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌)
28	27	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑌 ∈ 𝒫 𝑌)
29		foeq2 6804	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
30	29	exbidv 1955	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
31	30	rspcev 3580	. . . . . . . 8 ⊢ ((𝑌 ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
32	28, 31	sylancom 600	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
33	32	ex 418	. . . . . 6 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑧 𝑧:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
34	26, 33	biimtrid 245	. . . . 5 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
35		n0 4303	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝑋)
36	35	biimpi 219	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑤 𝑤 ∈ 𝑋)
37	36	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑤 𝑤 ∈ 𝑋)
38		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
39		difexg 5295	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ V → (𝑌 ∖ 𝑦) ∈ V)
40		vsnex 5397	. . . . . . . . . . . . . 14 ⊢ {𝑤} ∈ V
41		xpexg 7774	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∖ 𝑦) ∈ V ∧ {𝑤} ∈ V) → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
42	39, 40, 41	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
43		unexg 7770	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ V ∧ ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
44	38, 42, 43	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ V → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
45	44	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
46	45	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
47		fofn 6809	. . . . . . . . . . . . . . 15 ⊢ (𝑧:𝑦–onto→𝑋 → 𝑧 Fn 𝑦)
48	47	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋) → 𝑧 Fn 𝑦)
49	48	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → 𝑧 Fn 𝑦)
50		vex 3458	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
51		fnconstg 6781	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
52	50, 51	mp1i 14	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
53		disjdif 4429	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅
54	53	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅)
55	49, 52, 54	fnund 6665	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)))
56		elpwi 4567	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌)
57		undif 4441	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝑌 ↔ (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
58	56, 57	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝒫 𝑌 → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
59	58	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
60	59	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
61	60	fneq2d 6644	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)) ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌))
62	55, 61	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌)
63		rnun 6142	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤}))
64		forn 6810	. . . . . . . . . . . . . . . 16 ⊢ (𝑧:𝑦–onto→𝑋 → ran 𝑧 = 𝑋)
65	64	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ran 𝑧 = 𝑋)
66	65	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran 𝑧 = 𝑋)
67	66	uneq1d 4169	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})))
68		fconst6g 6782	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑋 → ((𝑌 ∖ 𝑦) × {𝑤}):(𝑌 ∖ 𝑦)⟶𝑋)
69	68	frnd 6729	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑋 → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
70	69	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
71		ssequn2 4190	. . . . . . . . . . . . . 14 ⊢ (ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋 ↔ (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
72	70, 71	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
73	67, 72	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
74	63, 73	eqtrid 2810	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
75		df-fo 6553	. . . . . . . . . . 11 ⊢ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋 ↔ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌 ∧ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋))
76	62, 74, 75	sylanbrc 595	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋)
77		foeq1 6803	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) → (𝑥:𝑌–onto→𝑋 ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋))
78	46, 76, 77	spcedv 3556	. . . . . . . . 9 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ∃𝑥 𝑥:𝑌–onto→𝑋)
79	37, 78	exlimddv 1969	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑥 𝑥:𝑌–onto→𝑋)
80	79	expr 462	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
81	80	exlimdv 1967	. . . . . 6 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
82	81	rexlimdva 3167	. . . . 5 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
83	34, 82	impbid 215	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
84	24, 83	bitrd 282	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
85	22, 84	pm2.61dane 3046	. 2 ⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
86	1, 85	syl 18	1 ⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2146   ≠ wne 2959  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588   class class class wbr 5106   × cxp 5653  ran crn 5656   Fn wfn 6542  –onto→wfo 6545  –1-1-onto→wf1o 6546   ≼^* cwdom 9571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-wdom 9572

This theorem is used by:  brwdom3  9589