Theorem weiunlem1 36376

Description: Lemma for weiunpo 36378, weiunso 36379, weiunfr 36382, and weiunse 36383. (Contributed by Matthew House, 23-Aug-2025.)

Hypothesis

Ref	Expression
weiunlem1.1	⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))

Assertion

Ref	Expression
weiunlem1	⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))

Distinct variable groups:   𝑢,𝐴,𝑣,𝑤,𝑥   𝑢,𝐵,𝑣,𝑤   𝑢,𝑅,𝑣,𝑤

Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunlem1

Step	Hyp	Ref	Expression
1		ssrab2 4097	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ⊆ 𝐴
2		eliun 5023	. . . . . . 7 ⊢ (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
3		rabn0 4408	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
4	2, 3	sylbb2 238	. . . . . 6 ⊢ (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ≠ ∅)
5		wereu2 5696	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ≠ ∅)) → ∃!𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
6	1, 5	mpanr1 702	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ≠ ∅) → ∃!𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
7	4, 6	sylan2 592	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃!𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
8		riotacl 7419	. . . . 5 ⊢ (∃!𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢 → (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵})
9	7, 8	syl 17	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵})
10	1, 9	sselid 4000	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) ∈ 𝐴)
11		weiunlem1.1	. . 3 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
12	10, 11	fmptd 7146	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
13		simpr 484	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
14	11	fvmpt2 7038	. . . . . . . 8 ⊢ ((𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}) → (𝐹‘𝑤) = (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
15	13, 9, 14	syl2anc 583	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝐹‘𝑤) = (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
16	15, 9	eqeltrd 2838	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝐹‘𝑤) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵})
17		nfcv 2904	. . . . . . 7 ⊢ Ⅎ𝑥𝐴
18	17	elrabsf 3847	. . . . . 6 ⊢ ((𝐹‘𝑤) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ↔ ((𝐹‘𝑤) ∈ 𝐴 ∧ [(𝐹‘𝑤) / 𝑥]𝑤 ∈ 𝐵))
19	16, 18	sylib 218	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ((𝐹‘𝑤) ∈ 𝐴 ∧ [(𝐹‘𝑤) / 𝑥]𝑤 ∈ 𝐵))
20	19	simprd 495	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → [(𝐹‘𝑤) / 𝑥]𝑤 ∈ 𝐵)
21		sbcel2 4437	. . . 4 ⊢ ([(𝐹‘𝑤) / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
22	20, 21	sylib 218	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
23	22	ralrimiva 3148	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
24	15	eqcomd 2740	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) = (𝐹‘𝑤))
25		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑢∪ 𝑥 ∈ 𝐴 𝐵
26		nfriota1 7408	. . . . . . . . . 10 ⊢ Ⅎ𝑢(℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
27	25, 26	nfmpt 5276	. . . . . . . . 9 ⊢ Ⅎ𝑢(𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
28	11, 27	nfcxfr 2902	. . . . . . . 8 ⊢ Ⅎ𝑢𝐹
29		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑢𝑤
30	28, 29	nffv 6929	. . . . . . 7 ⊢ Ⅎ𝑢(𝐹‘𝑤)
31		nfcv 2904	. . . . . . . 8 ⊢ Ⅎ𝑢{𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}
32		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑢𝑣
33		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑢𝑅
34	32, 33, 30	nfbr 5216	. . . . . . . . 9 ⊢ Ⅎ𝑢 𝑣𝑅(𝐹‘𝑤)
35	34	nfn 1856	. . . . . . . 8 ⊢ Ⅎ𝑢 ¬ 𝑣𝑅(𝐹‘𝑤)
36	31, 35	nfralw 3312	. . . . . . 7 ⊢ Ⅎ𝑢∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤)
37		nfcv 2904	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∪ 𝑥 ∈ 𝐴 𝐵
38		nfra1 3285	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢
39		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣{𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}
40	38, 39	nfriota 7414	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
41	37, 40	nfmpt 5276	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
42	11, 41	nfcxfr 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝐹
43		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑣𝑤
44	42, 43	nffv 6929	. . . . . . . . 9 ⊢ Ⅎ𝑣(𝐹‘𝑤)
45	44	nfeq2 2922	. . . . . . . 8 ⊢ Ⅎ𝑣 𝑢 = (𝐹‘𝑤)
46		breq2 5173	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑤) → (𝑣𝑅𝑢 ↔ 𝑣𝑅(𝐹‘𝑤)))
47	46	notbid 318	. . . . . . . 8 ⊢ (𝑢 = (𝐹‘𝑤) → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅(𝐹‘𝑤)))
48	45, 47	ralbid 3274	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑤) → (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤)))
49	30, 36, 48	riota2f 7426	. . . . . 6 ⊢ (((𝐹‘𝑤) ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ∧ ∃!𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) → (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤) ↔ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) = (𝐹‘𝑤)))
50	16, 7, 49	syl2anc 583	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤) ↔ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) = (𝐹‘𝑤)))
51	24, 50	mpbird 257	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤))
52	17	elrabsf 3847	. . . . . . . 8 ⊢ (𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ↔ (𝑣 ∈ 𝐴 ∧ [𝑣 / 𝑥]𝑤 ∈ 𝐵))
53		sbcel2 4437	. . . . . . . . 9 ⊢ ([𝑣 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵)
54	53	anbi2i 622	. . . . . . . 8 ⊢ ((𝑣 ∈ 𝐴 ∧ [𝑣 / 𝑥]𝑤 ∈ 𝐵) ↔ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵))
55	52, 54	bitri 275	. . . . . . 7 ⊢ (𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ↔ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵))
56	55	imbi1i 349	. . . . . 6 ⊢ ((𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵) → ¬ 𝑣𝑅(𝐹‘𝑤)))
57		impexp 450	. . . . . 6 ⊢ (((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵) → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ (𝑣 ∈ 𝐴 → (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
58	56, 57	bitri 275	. . . . 5 ⊢ ((𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ (𝑣 ∈ 𝐴 → (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
59	58	ralbii2 3091	. . . 4 ⊢ (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅(𝐹‘𝑤) ↔ ∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)))
60	51, 59	sylib 218	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)))
61	60	ralrimiva 3148	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)))
62	12, 23, 61	3jca 1128	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103   ≠ wne 2942  ∀wral 3063  ∃wrex 3072  ∃!wreu 3381  {crab 3438  [wsbc 3798  ⦋csb 3915   ⊆ wss 3970  ∅c0 4347  ∪ ciun 5019   class class class wbr 5169   ↦ cmpt 5252   Se wse 5652   We wwe 5653  ⟶wf 6568  ‘cfv 6572  ℩crio 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401

This theorem is referenced by:  weiunlem2  36377  weiunfrlem1  36380  weiunfrlem2  36381