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