Theorem disjinfi 45968

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
disjinfi.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
disjinfi.d	⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
disjinfi.c	⊢ (𝜑 → 𝐶 ∈ Fin)

Assertion

Ref	Expression
disjinfi	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝑉   𝜑,𝑥

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem disjinfi

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjinfi.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ Fin)
2		inss2 4190	. . 3 ⊢ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶
3		ssfi 9164	. . 3 ⊢ ((𝐶 ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin)
4	1, 2, 3	sylancl 598	. 2 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin)
5	2	a1i 11	. . . 4 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶)
6	1, 5	ssexd 5297	. . 3 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V)
7		elinel1 4154	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
8		eluni2 4878	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤)
9	8	biimpi 219	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤)
10		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
11	10	elrnmpt 5950	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵))
12	11	elv 3462	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)
13	12	birani 509	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)
14		nfmpt1 5212	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
15	14	nfrn 5944	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥ran (𝑥 ∈ 𝐴 ↦ 𝐵)
16	15	nfcri 2919	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
17		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑤
18	16, 17	nfan 1932	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤)
19		simpl 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝑤)
20		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑤 = 𝐵)
21	19, 20	eleqtrd 2867	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝐵)
22	21	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑤 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))
23	22	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑤 → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)))
24	23	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)))
25	18, 24	reximdai 3269	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
26	13, 25	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
27	26	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
29	28	rexlimdv 3166	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
30	9, 29	mpd 16	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
31	7, 30	syl 18	. . . . . . . . 9 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
32	31	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
33		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
34	15	nfuni 4881	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
35		nfcv 2927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
36	34, 35	nfin 4177	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)
37	36	nfcri 2919	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)
38	33, 37	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
39		nfre1 3292	. . . . . . . . 9 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)
40		elinel2 4155	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ 𝐶)
41		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴)
42		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
43		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐶)
44	42, 43	elind 4153	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶))
45		rspe 3257	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
46	41, 44, 45	3imp3i2an 1364	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
47	46	3exp 1137	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
48	40, 47	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
49	48	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
50	38, 39, 49	rexlimd 3274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
51	32, 50	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
52		disjinfi.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
53		disjors 5094	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
54	52, 53	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
55		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
56		nfcv 2927	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥𝐴
57		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑧 = 𝑤
58		nfcsb1v 3878	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
59		nfcv 2927	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝑤
60	59	nfcsb1 3877	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
61	58, 60	nfin 4177	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵)
62	61	nfeq1 2942	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅
63	57, 62	nfor 1937	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
64	56, 63	nfralw 3314	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
65		equequ1 2058	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
66		csbeq1a 3868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
67	66	ineq1d 4172	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵))
68	67	eqeq1d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
69	65, 68	orbi12d 932	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)))
70	69	ralbidv 3190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)))
71	55, 64, 70	cbvralw 3309	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
72	54, 71	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
73	72	r19.21bi 3259	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
74		rspa 3256	. . . . . . . . . . . . 13 ⊢ ((∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
75	74	orcomd 885	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤))
76	73, 75	sylan 592	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤))
77		elinel1 4154	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐵)
78		sbsbc 3750	. . . . . . . . . . . . . 14 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))
79		sbcel2 4383	. . . . . . . . . . . . . 14 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶))
80		csbin 4407	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)
81	80	eleq2i 2857	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶))
82	78, 79, 81	3bitri 300	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶))
83		elinel1 4154	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
84	82, 83	sylbi 220	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
85		inelcm 4425	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) ≠ ∅)
86	85	neneqd 2965	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
87	77, 84, 86	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
88		pm2.53 865	. . . . . . . . . . 11 ⊢ (((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ → 𝑥 = 𝑤))
89	76, 87, 88	syl2im 41	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
90	89	ralrimiva 3159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
91	90	ralrimiva 3159	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
92	91	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
93		reu2 3690	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)))
94	51, 92, 93	sylanbrc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
95		riotacl2 7392	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)})
96		nfriota1 7383	. . . . . . . . 9 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
97	96	nfcsb1 3877	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵
98	97, 35	nfin 4177	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)
99	98	nfcri 2919	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)
100		csbeq1a 3868	. . . . . . . . . . 11 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝐵 = ⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵)
101	100	ineq1d 4172	. . . . . . . . . 10 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝐵 ∩ 𝐶) = (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))
102	101	eleq2d 2851	. . . . . . . . 9 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)))
103	96, 56, 99, 102	elrabf 3649	. . . . . . . 8 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)))
104	103	simplbi 502	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴)
105	103	simprbi 503	. . . . . . . 8 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))
106	105	ne0d 4295	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)
107		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑥∅
108	98, 107	nfne 3063	. . . . . . . 8 ⊢ Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅
109	101	neeq1d 3019	. . . . . . . 8 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
110	96, 56, 108, 109	elrabf 3649	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
111	104, 106, 110	sylanbrc 595	. . . . . 6 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
112	94, 95, 111	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
113	112	ralrimiva 3159	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
114	60, 35	nfin 4177	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)
115	114, 107	nfne 3063	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅
116		csbeq1a 3868	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
117	116	ineq1d 4172	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
118	117	neeq1d 3019	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
119	59, 56, 115, 118	elrabf 3649	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (𝑤 ∈ 𝐴 ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
120	119	simprbi 503	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)
121		n0 4307	. . . . . . . . 9 ⊢ ((⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
122	120, 121	sylib 221	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
123	122	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
124	119	simplbi 502	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → 𝑤 ∈ 𝐴)
125		elinel1 4154	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
126	125	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
127		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 ∈ 𝐴)
128		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴)
129	60	nfel1 2943	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉
130	128, 129	nfim 1929	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
131		eleq1w 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
132	131	anbi2d 642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴)))
133	116	eleq1d 2850	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → (𝐵 ∈ 𝑉 ↔ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉))
134	132, 133	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)))
135		disjinfi.b	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
136	130, 134, 135	chvarfv 2279	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
137	136	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
138		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)
139	138	elrnmpt1 5952	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ 𝐴 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵))
140	127, 137, 139	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵))
141		nfcv 2927	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐵
142	116	equcoms 2053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
143	142	eqcomd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → ⦋𝑤 / 𝑥⦌𝐵 = 𝐵)
144	60, 141, 143	cbvmpt 5215	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
145	144	rneqi 5929	. . . . . . . . . . . . . 14 ⊢ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = ran (𝑥 ∈ 𝐴 ↦ 𝐵)
146	140, 145	eleqtrdi 2875	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
147		elunii 4879	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
148	126, 146, 147	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
149		elinel2 4155	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐶)
150	149	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐶)
151	148, 150	elind 4153	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
152		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ (𝐵 ∩ 𝐶)
153	114	nfcri 2919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)
154	117	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)))
155	152, 153, 154	cbvriotaw 7385	. . . . . . . . . . . 12 ⊢ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
156		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
157		rspe 3257	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
158	157	adantll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
159		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝜑)
160		sbequ 2120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)))
161		sbsbc 3750	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))
162	161	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)))
163		sbcel2 4383	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶))
164		csbin 4407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶)
165		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ V → ⦋𝑧 / 𝑥⦌𝐶 = 𝐶)
166	165	elv 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⦋𝑧 / 𝑥⦌𝐶 = 𝐶
167	166	ineq2i 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
168	164, 167	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
169	168	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
170	163, 169	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
171	170	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))
172	160, 162, 171	3bitrd 308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))
173	172	anbi2d 642	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))))
174		equequ2 2059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑧))
175	173, 174	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)))
176	175	cbvralvw 3245	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))
177	176	ralbii 3113	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))
178		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑤∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)
179	58, 35	nfin 4177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
180	179	nfcri 2919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
181	153, 180	nfan 1932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
182		nfv 1947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥 𝑤 = 𝑧
183	181, 182	nfim 1929	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)
184	56, 183	nfralw 3314	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)
185	154	anbi1d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))))
186		equequ1 2058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑧 ↔ 𝑤 = 𝑧))
187	185, 186	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
188	187	ralbidv 3190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
189	178, 184, 188	cbvralw 3309	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
190		sbsbc 3750	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
191		sbcel2 4383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
192		csbin 4407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶)
193		csbcow 3869	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
194		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ V → ⦋𝑧 / 𝑤⦌𝐶 = 𝐶)
195	194	elv 3462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⦋𝑧 / 𝑤⦌𝐶 = 𝐶
196	193, 195	ineq12i 4171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
197	192, 196	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
198	197	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
199	190, 191, 198	3bitrri 301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
200	199	anbi2i 635	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)))
201	200	imbi1i 352	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
202	201	2ralbii 3142	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
203	177, 189, 202	3bitri 300	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
204	92, 203	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
205	159, 151, 204	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
206		reu2 3690	. . . . . . . . . . . . . . 15 ⊢ (∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
207	158, 205, 206	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
208		riota1 7397	. . . . . . . . . . . . . 14 ⊢ (∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤))
209	207, 208	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤))
210	127, 156, 209	mpbi2and 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)
211	155, 210	eqtr2id 2813	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
212	151, 211	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
213	212	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
214	124, 213	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
215	214	eximdv 1950	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
216	123, 215	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
217		df-rex 3092	. . . . . 6 ⊢ (∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
218	216, 217	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
219	218	ralrimiva 3159	. . . 4 ⊢ (𝜑 → ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
220		eqid 2765	. . . . 5 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) = (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
221	220	fompt 7117	. . . 4 ⊢ ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
222	113, 219, 221	sylanbrc 595	. . 3 ⊢ (𝜑 → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
223		fodomg 10521	. . 3 ⊢ ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)))
224	6, 222, 223	sylc 66	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
225		domfi 9180	. 2 ⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)
226	4, 224, 225	syl2anc 596	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812  [wsb 2099   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  ∃!wreu 3369  {crab 3418  Vcvv 3457  [wsbc 3746  ⦋csb 3854   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  ∪ cuni 4874  Disj wdisj 5078   class class class wbr 5111   ↦ cmpt 5194  ran crn 5664  –onto→wfo 6538  ℩crio 7375   ≼ cdom 8947  Fincfn 8949

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-ac2 10462

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-disj 5079  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-1o 8459  df-er 8700  df-map 8832  df-en 8950  df-dom 8951  df-fin 8953  df-card 9941  df-acn 9944  df-ac 10116

This theorem is used by:  fsumiunss  46349  sge0iunmptlemre  47187