Theorem brwdom2 9167

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 3416	. 2 ⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ V)
2		0wdom 9164	. . . . . 6 ⊢ (𝑌 ∈ V → ∅ ≼* 𝑌)
3		breq1 5042	. . . . . 6 ⊢ (𝑋 = ∅ → (𝑋 ≼* 𝑌 ↔ ∅ ≼* 𝑌))
4	2, 3	syl5ibrcom 250	. . . . 5 ⊢ (𝑌 ∈ V → (𝑋 = ∅ → 𝑋 ≼* 𝑌))
5	4	imp 410	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → 𝑋 ≼* 𝑌)
6		0elpw 5232	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑌
7		f1o0 6675	. . . . . . . 8 ⊢ ∅:∅–1-1-onto→∅
8		f1ofo 6646	. . . . . . . 8 ⊢ (∅:∅–1-1-onto→∅ → ∅:∅–onto→∅)
9		0ex 5185	. . . . . . . . 9 ⊢ ∅ ∈ V
10		foeq1 6607	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (𝑧:∅–onto→∅ ↔ ∅:∅–onto→∅))
11	9, 10	spcev 3511	. . . . . . . 8 ⊢ (∅:∅–onto→∅ → ∃𝑧 𝑧:∅–onto→∅)
12	7, 8, 11	mp2b 10	. . . . . . 7 ⊢ ∃𝑧 𝑧:∅–onto→∅
13		foeq2 6608	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑧:𝑦–onto→∅ ↔ 𝑧:∅–onto→∅))
14	13	exbidv 1929	. . . . . . . 8 ⊢ (𝑦 = ∅ → (∃𝑧 𝑧:𝑦–onto→∅ ↔ ∃𝑧 𝑧:∅–onto→∅))
15	14	rspcev 3527	. . . . . . 7 ⊢ ((∅ ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:∅–onto→∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅)
16	6, 12, 15	mp2an 692	. . . . . 6 ⊢ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅
17		foeq3 6609	. . . . . . . 8 ⊢ (𝑋 = ∅ → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑦–onto→∅))
18	17	exbidv 1929	. . . . . . 7 ⊢ (𝑋 = ∅ → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑦–onto→∅))
19	18	rexbidv 3206	. . . . . 6 ⊢ (𝑋 = ∅ → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅))
20	16, 19	mpbiri 261	. . . . 5 ⊢ (𝑋 = ∅ → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
21	20	adantl 485	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
22	5, 21	2thd 268	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
23		brwdomn0 9163	. . . . 5 ⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
24	23	adantl 485	. . . 4 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋))
25		foeq1 6607	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥:𝑌–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
26	25	cbvexvw 2047	. . . . . 6 ⊢ (∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)
27		pwidg 4521	. . . . . . . . 9 ⊢ (𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌)
28	27	ad2antrr 726	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑌 ∈ 𝒫 𝑌)
29		foeq2 6608	. . . . . . . . . 10 ⊢ (𝑦 = 𝑌 → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋))
30	29	exbidv 1929	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
31	30	rspcev 3527	. . . . . . . 8 ⊢ ((𝑌 ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
32	28, 31	sylancom 591	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)
33	32	ex 416	. . . . . 6 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑧 𝑧:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
34	26, 33	syl5bi 245	. . . . 5 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
35		n0 4247	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝑋)
36	35	biimpi 219	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑤 𝑤 ∈ 𝑋)
37	36	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑤 𝑤 ∈ 𝑋)
38		vex 3402	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
39		difexg 5205	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ V → (𝑌 ∖ 𝑦) ∈ V)
40		snex 5309	. . . . . . . . . . . . . 14 ⊢ {𝑤} ∈ V
41		xpexg 7513	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∖ 𝑦) ∈ V ∧ {𝑤} ∈ V) → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
42	39, 40, 41	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V)
43		unexg 7512	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ V ∧ ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
44	38, 42, 43	sylancr 590	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ V → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
45	44	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
46	45	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V)
47		fofn 6613	. . . . . . . . . . . . . . 15 ⊢ (𝑧:𝑦–onto→𝑋 → 𝑧 Fn 𝑦)
48	47	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋) → 𝑧 Fn 𝑦)
49	48	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → 𝑧 Fn 𝑦)
50		vex 3402	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
51		fnconstg 6585	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
52	50, 51	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦))
53		disjdif 4372	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅
54	53	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅)
55	49, 52, 54	fnund 6469	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)))
56		elpwi 4508	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌)
57		undif 4382	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝑌 ↔ (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
58	56, 57	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝒫 𝑌 → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
59	58	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
60	59	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌)
61	60	fneq2d 6451	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)) ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌))
62	55, 61	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌)
63		rnun 5989	. . . . . . . . . . . 12 ⊢ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤}))
64		forn 6614	. . . . . . . . . . . . . . . 16 ⊢ (𝑧:𝑦–onto→𝑋 → ran 𝑧 = 𝑋)
65	64	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ran 𝑧 = 𝑋)
66	65	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran 𝑧 = 𝑋)
67	66	uneq1d 4062	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})))
68		fconst6g 6586	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑋 → ((𝑌 ∖ 𝑦) × {𝑤}):(𝑌 ∖ 𝑦)⟶𝑋)
69	68	frnd 6531	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝑋 → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
70	69	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋)
71		ssequn2 4083	. . . . . . . . . . . . . 14 ⊢ (ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋 ↔ (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
72	70, 71	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
73	67, 72	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
74	63, 73	syl5eq 2783	. . . . . . . . . . 11 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)
75		df-fo 6364	. . . . . . . . . . 11 ⊢ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋 ↔ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌 ∧ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋))
76	62, 74, 75	sylanbrc 586	. . . . . . . . . 10 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋)
77		foeq1 6607	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) → (𝑥:𝑌–onto→𝑋 ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋))
78	46, 76, 77	spcedv 3503	. . . . . . . . 9 ⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ∃𝑥 𝑥:𝑌–onto→𝑋)
79	37, 78	exlimddv 1943	. . . . . . . 8 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑥 𝑥:𝑌–onto→𝑋)
80	79	expr 460	. . . . . . 7 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
81	80	exlimdv 1941	. . . . . 6 ⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋))
82	81	rexlimdva 3193	. . . . 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 3019	. 2 ⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
86	1, 85	syl 17	1 ⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  ∃wrex 3052  Vcvv 3398   ∖ cdif 3850   ∪ cun 3851   ∩ cin 3852   ⊆ wss 3853  ∅c0 4223  𝒫 cpw 4499  {csn 4527   class class class wbr 5039   × cxp 5534  ran crn 5537   Fn wfn 6353  –onto→wfo 6356  –1-1-onto→wf1o 6357   ≼^* cwdom 9158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-wdom 9159

This theorem is referenced by:  brwdom3  9176