This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjinfi

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

Ref Expression
Hypotheses disjinfi.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
disjinfi.d ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
disjinfi.c ⊢ ( 𝜑 → 𝐶 ∈ Fin )
Assertion disjinfi ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∈ Fin )

Proof

Step Hyp Ref Expression
1 disjinfi.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 disjinfi.d ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
3 disjinfi.c ⊢ ( 𝜑 → 𝐶 ∈ Fin )
4 inss2 ⊢ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ⊆ 𝐶
5 ssfi ⊢ ( ( 𝐶 ∈ Fin ∧ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ⊆ 𝐶 ) → ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∈ Fin )
6 3 4 5 sylancl ⊢ ( 𝜑 → ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∈ Fin )
7 4 a1i ⊢ ( 𝜑 → ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ⊆ 𝐶 )
8 3 7 ssexd ⊢ ( 𝜑 → ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∈ V )
9 elinel1 ⊢ ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) → 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10 eluni2 ⊢ ( 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ∈ 𝑤 )
11 10 biimpi ⊢ ( 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ∈ 𝑤 )
12 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
13 12 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) )
14 13 elv ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
15 14 birani ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑦 ∈ 𝑤 ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
16 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
17 16 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
18 17 nfcri ⊢ Ⅎ 𝑥 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
19 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝑤
20 18 19 nfan ⊢ Ⅎ 𝑥 ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑦 ∈ 𝑤 )
21 simpl ⊢ ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵 ) → 𝑦 ∈ 𝑤 )
22 simpr ⊢ ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵 ) → 𝑤 = 𝐵 )
23 21 22 eleqtrd ⊢ ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵 ) → 𝑦 ∈ 𝐵 )
24 23 ex ⊢ ( 𝑦 ∈ 𝑤 → ( 𝑤 = 𝐵 → 𝑦 ∈ 𝐵 ) )
25 24 a1d ⊢ ( 𝑦 ∈ 𝑤 → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝑦 ∈ 𝐵 ) ) )
26 25 adantl ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑦 ∈ 𝑤 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝑦 ∈ 𝐵 ) ) )
27 20 26 reximdai ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑦 ∈ 𝑤 ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
28 15 27 mpd ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝑦 ∈ 𝑤 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
29 28 ex ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑦 ∈ 𝑤 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
30 29 a1i ⊢ ( 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑦 ∈ 𝑤 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) ) )
31 30 rexlimdv ⊢ ( 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ∈ 𝑤 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
32 11 31 mpd ⊢ ( 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
33 9 32 syl ⊢ ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
35 nfv ⊢ Ⅎ 𝑥 𝜑
36 17 nfuni ⊢ Ⅎ 𝑥 ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
37 nfcv ⊢ Ⅎ 𝑥 𝐶
38 36 37 nfin ⊢ Ⅎ 𝑥 ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 )
39 38 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 )
40 35 39 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) )
41 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 )
42 elinel2 ⊢ ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) → 𝑦 ∈ 𝐶 )
43 simp2 ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
44 simpr ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
45 simpl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐶 )
46 44 45 elind ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
47 rspe ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
48 43 46 47 3imp3i2an ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
49 48 3exp ⊢ ( 𝑦 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
50 42 49 syl ⊢ ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
52 40 41 51 rexlimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
53 34 52 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
54 disjors ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
55 2 54 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
56 nfv ⊢ Ⅎ 𝑧 ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
57 nfcv ⊢ Ⅎ 𝑥 𝐴
58 nfv ⊢ Ⅎ 𝑥 𝑧 = 𝑤
59 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
60 nfcv ⊢ Ⅎ 𝑥 𝑤
61 60 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
62 59 61 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
63 62 nfeq1 ⊢ Ⅎ 𝑥 ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅
64 58 63 nfor ⊢ Ⅎ 𝑥 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
65 57 64 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ 𝐴 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
66 equequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑧 = 𝑤 ) )
67 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
68 67 ineq1d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
69 68 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
70 66 69 orbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
71 70 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
72 56 65 71 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 = 𝑤 ∨ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
73 55 72 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
74 73 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
75 rspa ⊢ ( ( ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
76 75 orcomd ⊢ ( ( ∀ 𝑤 ∈ 𝐴 ( 𝑥 = 𝑤 ∨ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑥 = 𝑤 ) )
77 74 76 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑥 = 𝑤 ) )
78 elinel1 ⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑦 ∈ 𝐵 )
79 sbsbc ⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
80 sbcel2 ⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) )
81 csbin ⊢ ⦋ 𝑤 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐶 )
82 81 eleq2i ⊢ ( 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ) )
83 79 80 82 3bitri ⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ) )
84 elinel1 ⊢ ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐶 ) → 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
85 83 84 sylbi ⊢ ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
86 inelcm ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) → ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) ≠ ∅ )
87 86 neneqd ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) → ¬ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
88 78 85 87 syl2an ⊢ ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ¬ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
89 pm2.53 ⊢ ( ( ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑥 = 𝑤 ) → ( ¬ ( 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ → 𝑥 = 𝑤 ) )
90 77 88 89 syl2im ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) )
91 90 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) )
92 91 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) )
94 reu2 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) ) )
95 53 93 94 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ∃! 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
96 riotacl2 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } )
97 nfriota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
98 97 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵
99 98 37 nfin ⊢ Ⅎ 𝑥 ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
100 99 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
101 csbeq1a ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐵 = ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 )
102 101 ineq1d ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝐵 ∩ 𝐶 ) = ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
103 102 eleq2d ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
104 97 57 100 103 elrabf ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } ↔ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ 𝐴 ∧ 𝑦 ∈ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
105 104 simplbi ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } → ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ 𝐴 )
106 104 simprbi ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } → 𝑦 ∈ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
107 106 ne0d ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } → ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ )
108 nfcv ⊢ Ⅎ 𝑥 ∅
109 99 108 nfne ⊢ Ⅎ 𝑥 ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅
110 102 neeq1d ⊢ ( 𝑥 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
111 97 57 109 110 elrabf ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ↔ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ 𝐴 ∧ ( ⦋ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
112 105 107 111 sylanbrc ⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) } → ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } )
113 95 96 112 3syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } )
114 113 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } )
115 61 37 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
116 115 108 nfne ⊢ Ⅎ 𝑥 ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅
117 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
118 117 ineq1d ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
119 118 neeq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
120 60 57 116 119 elrabf ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ↔ ( 𝑤 ∈ 𝐴 ∧ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
121 120 simprbi ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } → ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ )
122 n0 ⊢ ( ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
123 121 122 sylib ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } → ∃ 𝑦 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ) → ∃ 𝑦 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
125 120 simplbi ⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } → 𝑤 ∈ 𝐴 )
126 elinel1 ⊢ ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
127 126 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
128 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 ∈ 𝐴 )
129 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ 𝐴 )
130 61 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉
131 129 130 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
132 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
133 132 anbi2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ) )
134 117 eleq1d ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
135 133 134 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) )
136 131 135 1 chvarfv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
137 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
138 eqid ⊢ ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
139 138 elrnmpt1 ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ ran ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
140 128 137 139 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ ran ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
141 nfcv ⊢ Ⅎ 𝑤 𝐵
142 117 equcoms ⊢ ( 𝑤 = 𝑥 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
143 142 eqcomd ⊢ ( 𝑤 = 𝑥 → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 = 𝐵 )
144 61 141 143 cbvmpt ⊢ ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
145 144 rneqi ⊢ ran ( 𝑤 ∈ 𝐴 ↦ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
146 140 145 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
147 elunii ⊢ ( ( 𝑦 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
148 127 146 147 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
149 elinel2 ⊢ ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → 𝑦 ∈ 𝐶 )
150 149 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
151 148 150 elind ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) )
152 nfv ⊢ Ⅎ 𝑤 𝑦 ∈ ( 𝐵 ∩ 𝐶 )
153 115 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
154 118 eleq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
155 152 153 154 cbvriotaw ⊢ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) = ( ℩ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
156 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
157 rspe ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ∃ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
158 157 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ∃ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
159 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝜑 )
160 sbequ ⊢ ( 𝑤 = 𝑧 → ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
161 sbsbc ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) )
162 161 a1i ⊢ ( 𝑤 = 𝑧 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
163 sbcel2 ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) )
164 csbin ⊢ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 )
165 csbconstg ⊢ ( 𝑧 ∈ V → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝐶 )
166 165 elv ⊢ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝐶
167 166 ineq2i ⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
168 164 167 eqtri ⊢ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
169 168 eleq2i ⊢ ( 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
170 163 169 bitri ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
171 170 a1i ⊢ ( 𝑤 = 𝑧 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
172 160 162 171 3bitrd ⊢ ( 𝑤 = 𝑧 → ( [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
173 172 anbi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ) )
174 equequ2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑧 ) )
175 173 174 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) ↔ ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) ) )
176 175 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) )
177 176 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) )
178 nfv ⊢ Ⅎ 𝑤 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 )
179 59 37 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
180 179 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
181 153 180 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
182 nfv ⊢ Ⅎ 𝑥 𝑤 = 𝑧
183 181 182 nfim ⊢ Ⅎ 𝑥 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 )
184 57 183 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 )
185 154 anbi1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ) )
186 equequ1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑧 ↔ 𝑤 = 𝑧 ) )
187 185 186 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) ↔ ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) ) )
188 187 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) ) )
189 178 184 188 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
190 sbsbc ⊢ ( [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ↔ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
191 sbcel2 ⊢ ( [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ⦋ 𝑧 / 𝑤 ⦌ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
192 csbin ⊢ ⦋ 𝑧 / 𝑤 ⦌ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑧 / 𝑤 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑤 ⦌ 𝐶 )
193 csbcow ⊢ ⦋ 𝑧 / 𝑤 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵
194 csbconstg ⊢ ( 𝑧 ∈ V → ⦋ 𝑧 / 𝑤 ⦌ 𝐶 = 𝐶 )
195 194 elv ⊢ ⦋ 𝑧 / 𝑤 ⦌ 𝐶 = 𝐶
196 193 195 ineq12i ⊢ ( ⦋ 𝑧 / 𝑤 ⦌ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑤 ⦌ 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
197 192 196 eqtri ⊢ ⦋ 𝑧 / 𝑤 ⦌ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
198 197 eleq2i ⊢ ( 𝑦 ∈ ⦋ 𝑧 / 𝑤 ⦌ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ↔ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
199 190 191 198 3bitrri ⊢ ( 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ↔ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
200 199 anbi2i ⊢ ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) )
201 200 imbi1i ⊢ ( ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) ↔ ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
202 201 2ralbii ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ 𝑦 ∈ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
203 177 189 202 3bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ∧ [ 𝑤 / 𝑥 ] 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
204 93 203 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
205 159 151 204 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) )
206 reu2 ⊢ ( ∃! 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ↔ ( ∃ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ∧ [ 𝑧 / 𝑤 ] 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = 𝑧 ) ) )
207 158 205 206 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ∃! 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
208 riota1 ⊢ ( ∃! 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ↔ ( ℩ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) = 𝑤 ) )
209 207 208 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) ↔ ( ℩ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) = 𝑤 ) )
210 128 156 209 mpbi2and ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ( ℩ 𝑤 ∈ 𝐴 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) = 𝑤 )
211 155 210 eqtr2id ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
212 151 211 jca ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) ) → ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
213 212 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) ) )
214 125 213 sylan2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ) → ( 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) ) )
215 214 eximdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ) → ( ∃ 𝑦 𝑦 ∈ ( ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) → ∃ 𝑦 ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) ) )
216 124 215 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ) → ∃ 𝑦 ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
217 df-rex ⊢ ( ∃ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∧ 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
218 216 217 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ) → ∃ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
219 218 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∃ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
220 eqid ⊢ ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ↦ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) = ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ↦ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
221 220 fompt ⊢ ( ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ↦ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) : ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) –onto→ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ↔ ( ∀ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∧ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∃ 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) 𝑤 = ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
222 114 219 221 sylanbrc ⊢ ( 𝜑 → ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ↦ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) : ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) –onto→ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } )
223 fodomg ⊢ ( ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∈ V → ( ( 𝑦 ∈ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ↦ ( ℩ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) : ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) –onto→ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ≼ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) )
224 8 222 223 sylc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ≼ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) )
225 domfi ⊢ ( ( ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ∈ Fin ∧ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ≼ ( ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∩ 𝐶 ) ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∈ Fin )
226 6 224 225 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∩ 𝐶 ) ≠ ∅ } ∈ Fin )