Metamath Proof Explorer

Theorem disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . The proof uses fodomfi rather than fodomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

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