Theorem disjinfi 43402

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 4189	. . 3 ⊢ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶
3		ssfi 9117	. . 3 ⊢ ((𝐶 ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin)
4	1, 2, 3	sylancl 586	. 2 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin)
5	2	a1i 11	. . . 4 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶)
6	1, 5	ssexd 5281	. . 3 ⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V)
7		elinel1 4155	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
8		eluni2 4869	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤)
9	8	biimpi 215	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤)
10		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
11	10	elrnmpt 5911	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵))
12	11	elv 3451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)
13	12	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)
14	13	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)
15		nfmpt1 5213	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
16	15	nfrn 5907	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥ran (𝑥 ∈ 𝐴 ↦ 𝐵)
17	16	nfcri 2894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
18		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑤
19	17, 18	nfan 1902	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤)
20		simpl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝑤)
21		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑤 = 𝐵)
22	20, 21	eleqtrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝐵)
23	22	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑤 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))
24	23	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑤 → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)))
25	24	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)))
26	19, 25	reximdai 3244	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
27	14, 26	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
28	27	ex 413	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)))
30	29	rexlimdv 3150	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
31	9, 30	mpd 15	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
32	7, 31	syl 17	. . . . . . . . 9 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
33	32	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
34		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
35	16	nfuni 4872	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
36		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
37	35, 36	nfin 4176	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)
38	37	nfcri 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)
39	34, 38	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
40		nfre1 3268	. . . . . . . . 9 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)
41		elinel2 4156	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ 𝐶)
42		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴)
43		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
44		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐶)
45	43, 44	elind 4154	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶))
46		rspe 3232	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
47	42, 45, 46	3imp3i2an 1345	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
48	47	3exp 1119	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
49	41, 48	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
50	49	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
51	39, 40, 50	rexlimd 3249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
52	33, 51	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
53		disjinfi.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
54		disjors 5086	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
55	53, 54	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
56		nfv 1917	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
57		nfcv 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥𝐴
58		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥 𝑧 = 𝑤
59		nfcsb1v 3880	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
60		nfcv 2907	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝑤
61	60	nfcsb1 3879	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
62	59, 61	nfin 4176	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵)
63	62	nfeq1 2922	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅
64	58, 63	nfor 1907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
65	57, 64	nfralw 3294	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
66		equequ1 2028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤))
67		csbeq1a 3869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
68	67	ineq1d 4171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵))
69	68	eqeq1d 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
70	66, 69	orbi12d 917	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)))
71	70	ralbidv 3174	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)))
72	56, 65, 71	cbvralw 3289	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
73	55, 72	sylibr 233	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
74	73	r19.21bi 3234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
75		rspa 3231	. . . . . . . . . . . . 13 ⊢ ((∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))
76	75	orcomd 869	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤))
77	74, 76	sylan 580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤))
78		elinel1 4155	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐵)
79		sbsbc 3743	. . . . . . . . . . . . . 14 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))
80		sbcel2 4375	. . . . . . . . . . . . . 14 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶))
81		csbin 4399	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)
82	81	eleq2i 2829	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶))
83	79, 80, 82	3bitri 296	. . . . . . . . . . . . 13 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶))
84		elinel1 4155	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
85	83, 84	sylbi 216	. . . . . . . . . . . 12 ⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86		inelcm 4424	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) ≠ ∅)
87	86	neneqd 2948	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
88	78, 85, 87	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)
89		pm2.53 849	. . . . . . . . . . 11 ⊢ (((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ → 𝑥 = 𝑤))
90	77, 88, 89	syl2im 40	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
91	90	ralrimiva 3143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
92	91	ralrimiva 3143	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
93	92	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))
94		reu2 3683	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)))
95	52, 93, 94	sylanbrc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
96		riotacl2 7330	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)})
97		nfriota1 7320	. . . . . . . . 9 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
98	97	nfcsb1 3879	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵
99	98, 36	nfin 4176	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)
100	99	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)
101		csbeq1a 3869	. . . . . . . . . . 11 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝐵 = ⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵)
102	101	ineq1d 4171	. . . . . . . . . 10 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝐵 ∩ 𝐶) = (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))
103	102	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)))
104	97, 57, 100, 103	elrabf 3641	. . . . . . . 8 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)))
105	104	simplbi 498	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴)
106	104	simprbi 497	. . . . . . . 8 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))
107	106	ne0d 4295	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)
108		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑥∅
109	99, 108	nfne 3045	. . . . . . . 8 ⊢ Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅
110	102	neeq1d 3003	. . . . . . . 8 ⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
111	97, 57, 109, 110	elrabf 3641	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
112	105, 107, 111	sylanbrc 583	. . . . . 6 ⊢ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
113	95, 96, 112	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
114	113	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
115	61, 36	nfin 4176	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)
116	115, 108	nfne 3045	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅
117		csbeq1a 3869	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
118	117	ineq1d 4171	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
119	118	neeq1d 3003	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
120	60, 57, 116, 119	elrabf 3641	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (𝑤 ∈ 𝐴 ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅))
121	120	simprbi 497	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)
122		n0 4306	. . . . . . . . 9 ⊢ ((⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
123	121, 122	sylib 217	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
124	123	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
125	120	simplbi 498	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → 𝑤 ∈ 𝐴)
126		elinel1 4155	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
127	126	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)
128		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 ∈ 𝐴)
129		nfv 1917	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴)
130	61	nfel1 2923	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉
131	129, 130	nfim 1899	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
132		eleq1w 2820	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
133	132	anbi2d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴)))
134	117	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑤 → (𝐵 ∈ 𝑉 ↔ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉))
135	133, 134	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)))
136		disjinfi.b	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
137	131, 135, 136	chvarfv 2233	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
138	137	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)
139		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)
140	139	elrnmpt1 5913	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ 𝐴 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵))
141	128, 138, 140	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵))
142		nfcv 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐵
143	117	equcoms 2023	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
144	143	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → ⦋𝑤 / 𝑥⦌𝐵 = 𝐵)
145	61, 142, 144	cbvmpt 5216	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
146	145	rneqi 5892	. . . . . . . . . . . . . 14 ⊢ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = ran (𝑥 ∈ 𝐴 ↦ 𝐵)
147	141, 146	eleqtrdi 2848	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
148		elunii 4870	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
149	127, 147, 148	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
150		elinel2 4156	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐶)
151	150	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐶)
152	149, 151	elind 4154	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
153		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ (𝐵 ∩ 𝐶)
154	115	nfcri 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)
155	118	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)))
156	153, 154, 155	cbvriotaw 7322	. . . . . . . . . . . 12 ⊢ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
157		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
158		rspe 3232	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
159	158	adantll 712	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
160		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝜑)
161		sbequ 2086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)))
162		sbsbc 3743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)))
164		sbcel2 4375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶))
165		csbin 4399	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶)
166		csbconstg 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ V → ⦋𝑧 / 𝑥⦌𝐶 = 𝐶)
167	166	elv 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⦋𝑧 / 𝑥⦌𝐶 = 𝐶
168	167	ineq2i 4169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
169	165, 168	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
170	169	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
171	164, 170	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))
173	161, 163, 172	3bitrd 304	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))
174	173	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))))
175		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑧))
176	174, 175	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)))
177	176	cbvralvw 3225	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))
178	177	ralbii 3096	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))
179		nfv 1917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑤∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)
180	59, 36	nfin 4176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
181	180	nfcri 2894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
182	154, 181	nfan 1902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
183		nfv 1917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥 𝑤 = 𝑧
184	182, 183	nfim 1899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)
185	57, 184	nfralw 3294	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)
186	155	anbi1d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))))
187		equequ1 2028	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑧 ↔ 𝑤 = 𝑧))
188	186, 187	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
189	188	ralbidv 3174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
190	179, 185, 189	cbvralw 3289	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
191		sbsbc 3743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
192		sbcel2 4375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
193		csbin 4399	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶)
194		csbcow 3870	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵
195		csbconstg 3874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ V → ⦋𝑧 / 𝑤⦌𝐶 = 𝐶)
196	195	elv 3451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⦋𝑧 / 𝑤⦌𝐶 = 𝐶
197	194, 196	ineq12i 4170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
198	193, 197	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)
199	198	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))
200	191, 192, 199	3bitrri 297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
201	200	anbi2i 623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)))
202	201	imbi1i 349	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
203	202	2ralbii 3127	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
204	178, 190, 203	3bitri 296	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
205	93, 204	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
206	160, 152, 205	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))
207		reu2 3683	. . . . . . . . . . . . . . 15 ⊢ (∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)))
208	159, 206, 207	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))
209		riota1 7335	. . . . . . . . . . . . . 14 ⊢ (∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤))
210	208, 209	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤))
211	128, 157, 210	mpbi2and 710	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)
212	156, 211	eqtr2id 2789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
213	152, 212	jca 512	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
214	213	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
215	125, 214	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
216	215	eximdv 1920	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))))
217	124, 216	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
218		df-rex 3074	. . . . . 6 ⊢ (∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ ∃𝑦(𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
219	217, 218	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
220	219	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
221		eqid 2736	. . . . 5 ⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) = (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))
222	221	fompt 43401	. . . 4 ⊢ ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))
223	114, 220, 222	sylanbrc 583	. . 3 ⊢ (𝜑 → (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅})
224		fodomg 10458	. . 3 ⊢ ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)))
225	6, 223, 224	sylc 65	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))
226		domfi 9136	. 2 ⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)
227	4, 225, 226	syl2anc 584	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  ∃wex 1781  [wsb 2067   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  ∃!wreu 3351  {crab 3407  Vcvv 3445  [wsbc 3739  ⦋csb 3855   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  ∪ cuni 4865  Disj wdisj 5070   class class class wbr 5105   ↦ cmpt 5188  ran crn 5634  –onto→wfo 6494  ℩crio 7312   ≼ cdom 8881  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-ac2 10399

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-fin 8887  df-card 9875  df-acn 9878  df-ac 10052

This theorem is referenced by:  fsumiunss  43806  sge0iunmptlemre  44646