Theorem brwdom2 9400

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 3459	. 2 ⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ V)
2		0wdom 9397	. . . . . 6 ⊢ (𝑌 ∈ V → ∅ ≼* 𝑌)
3		breq1 5088	. . . . . 6 ⊢ (𝑋 = ∅ → (𝑋 ≼* 𝑌 ↔ ∅ ≼* 𝑌))
4	2, 3	syl5ibrcom 246	. . . . 5 ⊢ (𝑌 ∈ V → (𝑋 = ∅ → 𝑋 ≼* 𝑌))
5	4	imp 407	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → 𝑋 ≼* 𝑌)
6		0elpw 5291	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑌
7		f1o0 6788	. . . . . . . 8 ⊢ ∅:∅–1-1-onto→∅
8		f1ofo 6758	. . . . . . . 8 ⊢ (∅:∅–1-1-onto→∅ → ∅:∅–onto→∅)
9		0ex 5244	. . . . . . . . 9 ⊢ ∅ ∈ V
10		foeq1 6719	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (𝑧:∅–onto→∅ ↔ ∅:∅–onto→∅))
11	9, 10	spcev 3554	. . . . . . . 8 ⊢ (∅:∅–onto→∅ → ∃𝑧 𝑧:∅–onto→∅)
12	7, 8, 11	mp2b 10	. . . . . . 7 ⊢ ∃𝑧 𝑧:∅–onto→∅
13		foeq2 6720	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑧:𝑦–onto→∅ ↔ 𝑧:∅–onto→∅))
14	13	exbidv 1923	. . . . . . . 8 ⊢ (𝑦 = ∅ → (∃𝑧 𝑧:𝑦–onto→∅ ↔ ∃𝑧 𝑧:∅–onto→∅))
15	14	rspcev 3570	. . . . . . 7 ⊢ ((∅ ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:∅–onto→∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅)
16	6, 12, 15	mp2an 689	. . . . . 6 ⊢ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅
17		foeq3 6721	. . . . . . . 8 ⊢ (𝑋 = ∅ → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑦–onto→∅))
18	17	exbidv 1923	. . . . . . 7 ⊢ (𝑋 = ∅ → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑦–onto→∅))
19	18	rexbidv 3172	. . . . . 6 ⊢ (𝑋 = ∅ → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅))
20	16, 19	mpbiri 257	. . . . 5 ⊢ (𝑋 = ∅ → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
21	20	adantl 482	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
22	5, 21	2thd 264	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
23		brwdomn0 9396	. . . . 5 ⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
24	23	adantl 482	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
25		foeq1 6719	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥:𝑌–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
26	25	cbvexvw 2039	. . . . . 6 ⊢ (∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)
27		pwidg 4563	. . . . . . . . 9 ⊢ (𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌)
28	27	ad2antrr 723	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑌 ∈ 𝒫 𝑌)
29		foeq2 6720	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
30	29	exbidv 1923	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
31	30	rspcev 3570	. . . . . . . 8 ⊢ ((𝑌 ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
32	28, 31	sylancom 588	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
33	32	ex 413	. . . . . 6 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑧 𝑧:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
34	26, 33	biimtrid 241	. . . . 5 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
35		n0 4290	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝑋)
36	35	biimpi 215	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑤 𝑤 ∈ 𝑋)
37	36	ad2antlr 724	. . . . . . . . 9 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑤 𝑤 ∈ 𝑋)
38		vex 3445	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
39		difexg 5264	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ V → (𝑌 ∖ 𝑦) ∈ V)
40		snex 5367	. . . . . . . . . . . . . 14 ⊢ {𝑤} ∈ V
41		xpexg 7638	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∖ 𝑦) ∈ V ∧ {𝑤} ∈ V) → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
42	39, 40, 41	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
43		unexg 7637	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ V ∧ ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
44	38, 42, 43	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ V → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
45	44	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
46	45	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
47		fofn 6725	. . . . . . . . . . . . . . 15 ⊢ (𝑧:𝑦–onto→𝑋 → 𝑧 Fn 𝑦)
48	47	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋) → 𝑧 Fn 𝑦)
49	48	ad2antlr 724	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → 𝑧 Fn 𝑦)
50		vex 3445	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
51		fnconstg 6697	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
52	50, 51	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
53		disjdif 4415	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅
54	53	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅)
55	49, 52, 54	fnund 6582	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)))
56		elpwi 4550	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌)
57		undif 4425	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝑌 ↔ (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
58	56, 57	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝒫 𝑌 → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
59	58	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
60	59	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
61	60	fneq2d 6563	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)) ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌))
62	55, 61	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌)
63		rnun 6069	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤}))
64		forn 6726	. . . . . . . . . . . . . . . 16 ⊢ (𝑧:𝑦–onto→𝑋 → ran 𝑧 = 𝑋)
65	64	ad2antll 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ran 𝑧 = 𝑋)
66	65	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran 𝑧 = 𝑋)
67	66	uneq1d 4106	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})))
68		fconst6g 6698	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑋 → ((𝑌 ∖ 𝑦) × {𝑤}):(𝑌 ∖ 𝑦)⟶𝑋)
69	68	frnd 6643	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑋 → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
70	69	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
71		ssequn2 4127	. . . . . . . . . . . . . 14 ⊢ (ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋 ↔ (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
72	70, 71	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
73	67, 72	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
74	63, 73	eqtrid 2789	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
75		df-fo 6469	. . . . . . . . . . 11 ⊢ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋 ↔ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌 ∧ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋))
76	62, 74, 75	sylanbrc 583	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋)
77		foeq1 6719	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) → (𝑥:𝑌–onto→𝑋 ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋))
78	46, 76, 77	spcedv 3546	. . . . . . . . 9 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ∃𝑥 𝑥:𝑌–onto→𝑋)
79	37, 78	exlimddv 1937	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑥 𝑥:𝑌–onto→𝑋)
80	79	expr 457	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
81	80	exlimdv 1935	. . . . . 6 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
82	81	rexlimdva 3149	. . . . 5 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
83	34, 82	impbid 211	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
84	24, 83	bitrd 278	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
85	22, 84	pm2.61dane 3030	. 2 ⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
86	1, 85	syl 17	1 ⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540  ∃wex 1780   ∈ wcel 2105   ≠ wne 2941  ∃wrex 3071  Vcvv 3441   ∖ cdif 3893   ∪ cun 3894   ∩ cin 3895   ⊆ wss 3896  ∅c0 4266  𝒫 cpw 4543  {csn 4569   class class class wbr 5085   × cxp 5603  ran crn 5606   Fn wfn 6458  –onto→wfo 6461  –1-1-onto→wf1o 6462   ≼^* cwdom 9391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-wdom 9392

This theorem is referenced by:  brwdom3  9409