Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjinfi Structured version   Visualization version   GIF version

Theorem disjinfi 44556
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.
StepHypRef Expression
1 disjinfi.c . . 3 (𝜑𝐶 ∈ Fin)
2 inss2 4226 . . 3 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
3 ssfi 9192 . . 3 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
41, 2, 3sylancl 585 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
52a1i 11 . . . 4 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
61, 5ssexd 5319 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
7 elinel1 4192 . . . . . . . . . 10 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
8 eluni2 4908 . . . . . . . . . . . 12 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
98biimpi 215 . . . . . . . . . . 11 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
10 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1110elrnmpt 5953 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1211elv 3476 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1312biimpi 215 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
1413adantr 480 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
15 nfmpt1 5251 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑥𝐴𝐵)
1615nfrn 5949 . . . . . . . . . . . . . . . . . 18 𝑥ran (𝑥𝐴𝐵)
1716nfcri 2886 . . . . . . . . . . . . . . . . 17 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
18 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑥 𝑦𝑤
1917, 18nfan 1895 . . . . . . . . . . . . . . . 16 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
20 simpl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
21 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2220, 21eleqtrd 2831 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
2322ex 412 . . . . . . . . . . . . . . . . . 18 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
2423a1d 25 . . . . . . . . . . . . . . . . 17 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
2524adantl 481 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
2619, 25reximdai 3254 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
2714, 26mpd 15 . . . . . . . . . . . . . 14 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
2827ex 412 . . . . . . . . . . . . 13 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
2928a1i 11 . . . . . . . . . . . 12 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3029rexlimdv 3149 . . . . . . . . . . 11 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
319, 30mpd 15 . . . . . . . . . 10 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
327, 31syl 17 . . . . . . . . 9 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
3332adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
34 nfv 1910 . . . . . . . . . 10 𝑥𝜑
3516nfuni 4911 . . . . . . . . . . . 12 𝑥 ran (𝑥𝐴𝐵)
36 nfcv 2899 . . . . . . . . . . . 12 𝑥𝐶
3735, 36nfin 4213 . . . . . . . . . . 11 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
3837nfcri 2886 . . . . . . . . . 10 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
3934, 38nfan 1895 . . . . . . . . 9 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
40 nfre1 3278 . . . . . . . . 9 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
41 elinel2 4193 . . . . . . . . . . 11 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
42 simp2 1135 . . . . . . . . . . . . 13 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
43 simpr 484 . . . . . . . . . . . . . 14 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
44 simpl 482 . . . . . . . . . . . . . 14 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
4543, 44elind 4191 . . . . . . . . . . . . 13 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
46 rspe 3242 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
4742, 45, 463imp3i2an 1343 . . . . . . . . . . . 12 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
48473exp 1117 . . . . . . . . . . 11 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
4941, 48syl 17 . . . . . . . . . 10 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5049adantl 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5139, 40, 50rexlimd 3259 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
5233, 51mpd 15 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
53 disjinfi.d . . . . . . . . . . . . . . 15 (𝜑Disj 𝑥𝐴 𝐵)
54 disjors 5124 . . . . . . . . . . . . . . 15 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
5553, 54sylib 217 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
56 nfv 1910 . . . . . . . . . . . . . . 15 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
57 nfcv 2899 . . . . . . . . . . . . . . . 16 𝑥𝐴
58 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑥 𝑧 = 𝑤
59 nfcsb1v 3915 . . . . . . . . . . . . . . . . . . 19 𝑥𝑧 / 𝑥𝐵
60 nfcv 2899 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑤
6160nfcsb1 3914 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵
6259, 61nfin 4213 . . . . . . . . . . . . . . . . . 18 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
6362nfeq1 2914 . . . . . . . . . . . . . . . . 17 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
6458, 63nfor 1900 . . . . . . . . . . . . . . . 16 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
6557, 64nfralw 3304 . . . . . . . . . . . . . . 15 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
66 equequ1 2021 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
67 csbeq1a 3904 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
6867ineq1d 4208 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
6968eqeq1d 2730 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7066, 69orbi12d 917 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
7170ralbidv 3173 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
7256, 65, 71cbvralw 3299 . . . . . . . . . . . . . 14 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7355, 72sylibr 233 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
7473r19.21bi 3244 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
75 rspa 3241 . . . . . . . . . . . . 13 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
7675orcomd 870 . . . . . . . . . . . 12 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
7774, 76sylan 579 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
78 elinel1 4192 . . . . . . . . . . . 12 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
79 sbsbc 3779 . . . . . . . . . . . . . 14 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
80 sbcel2 4412 . . . . . . . . . . . . . 14 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
81 csbin 4436 . . . . . . . . . . . . . . 15 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
8281eleq2i 2821 . . . . . . . . . . . . . 14 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
8379, 80, 823bitri 297 . . . . . . . . . . . . 13 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
84 elinel1 4192 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
8583, 84sylbi 216 . . . . . . . . . . . 12 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
86 inelcm 4461 . . . . . . . . . . . . 13 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
8786neneqd 2941 . . . . . . . . . . . 12 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
8878, 85, 87syl2an 595 . . . . . . . . . . 11 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
89 pm2.53 850 . . . . . . . . . . 11 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
9077, 88, 89syl2im 40 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
9190ralrimiva 3142 . . . . . . . . 9 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
9291ralrimiva 3142 . . . . . . . 8 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
9392adantr 480 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
94 reu2 3719 . . . . . . 7 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
9552, 93, 94sylanbrc 582 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
96 riotacl2 7388 . . . . . 6 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
97 nfriota1 7378 . . . . . . . . 9 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
9897nfcsb1 3914 . . . . . . . . . . 11 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
9998, 36nfin 4213 . . . . . . . . . 10 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
10099nfcri 2886 . . . . . . . . 9 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
101 csbeq1a 3904 . . . . . . . . . . 11 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
102101ineq1d 4208 . . . . . . . . . 10 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
103102eleq2d 2815 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
10497, 57, 100, 103elrabf 3677 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
105104simplbi 497 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
106104simprbi 496 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
107106ne0d 4332 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
108 nfcv 2899 . . . . . . . . 9 𝑥
10999, 108nfne 3039 . . . . . . . 8 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
110102neeq1d 2996 . . . . . . . 8 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
11197, 57, 109, 110elrabf 3677 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
112105, 107, 111sylanbrc 582 . . . . . 6 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
11395, 96, 1123syl 18 . . . . 5 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
114113ralrimiva 3142 . . . 4 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
11561, 36nfin 4213 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶)
116115, 108nfne 3039 . . . . . . . . . . 11 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
117 csbeq1a 3904 . . . . . . . . . . . . 13 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
118117ineq1d 4208 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
119118neeq1d 2996 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
12060, 57, 116, 119elrabf 3677 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
121120simprbi 496 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
122 n0 4343 . . . . . . . . 9 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
123121, 122sylib 217 . . . . . . . 8 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
124123adantl 481 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
125120simplbi 497 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
126 elinel1 4192 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
127126adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
128 simplr 768 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
129 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑥(𝜑𝑤𝐴)
13061nfel1 2915 . . . . . . . . . . . . . . . . . 18 𝑥𝑤 / 𝑥𝐵𝑉
131129, 130nfim 1892 . . . . . . . . . . . . . . . . 17 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
132 eleq1w 2812 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
133132anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
134117eleq1d 2814 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
135133, 134imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
136 disjinfi.b . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵𝑉)
137131, 135, 136chvarfv 2229 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
138137adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
139 eqid 2728 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
140139elrnmpt1 5955 . . . . . . . . . . . . . . 15 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
141128, 138, 140syl2anc 583 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
142 nfcv 2899 . . . . . . . . . . . . . . . 16 𝑤𝐵
143117equcoms 2016 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
144143eqcomd 2734 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
14561, 142, 144cbvmpt 5254 . . . . . . . . . . . . . . 15 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
146145rneqi 5934 . . . . . . . . . . . . . 14 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
147141, 146eleqtrdi 2839 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
148 elunii 4909 . . . . . . . . . . . . 13 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
149127, 147, 148syl2anc 583 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
150 elinel2 4193 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
151150adantl 481 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
152149, 151elind 4191 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
153 nfv 1910 . . . . . . . . . . . . 13 𝑤 𝑦 ∈ (𝐵𝐶)
154115nfcri 2886 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
155118eleq2d 2815 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
156153, 154, 155cbvriotaw 7380 . . . . . . . . . . . 12 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
157 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
158 rspe 3242 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
159158adantll 713 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
160 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
161 sbequ 2079 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
162 sbsbc 3779 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
164 sbcel2 4412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
165 csbin 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
166 csbconstg 3909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
167166elv 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥𝐶 = 𝐶
168167ineq2i 4206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
169165, 168eqtri 2756 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
170169eleq2i 2821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
171164, 170bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
173161, 163, 1723bitrd 305 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
174173anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
175 equequ2 2022 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
176174, 175imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
177176cbvralvw 3230 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
178177ralbii 3089 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
179 nfv 1910 . . . . . . . . . . . . . . . . . . 19 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
18059, 36nfin 4213 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝐶)
181180nfcri 2886 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
182154, 181nfan 1895 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
183 nfv 1910 . . . . . . . . . . . . . . . . . . . . 21 𝑥 𝑤 = 𝑧
184182, 183nfim 1892 . . . . . . . . . . . . . . . . . . . 20 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
18557, 184nfralw 3304 . . . . . . . . . . . . . . . . . . 19 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
186155anbi1d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
187 equequ1 2021 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
188186, 187imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
189188ralbidv 3173 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
190179, 185, 189cbvralw 3299 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
191 sbsbc 3779 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
192 sbcel2 4412 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
193 csbin 4436 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
194 csbcow 3905 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
195 csbconstg 3909 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
196195elv 3476 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 / 𝑤𝐶 = 𝐶
197194, 196ineq12i 4207 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
198193, 197eqtri 2756 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
199198eleq2i 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
200191, 192, 1993bitrri 298 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
201200anbi2i 622 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
202201imbi1i 349 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
2032022ralbii 3124 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
204178, 190, 2033bitri 297 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
20593, 204sylib 217 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
206160, 152, 205syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
207 reu2 3719 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
208159, 206, 207sylanbrc 582 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
209 riota1 7393 . . . . . . . . . . . . . 14 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
210208, 209syl 17 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
211128, 157, 210mpbi2and 711 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
212156, 211eqtr2id 2781 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
213152, 212jca 511 . . . . . . . . . 10 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
214213ex 412 . . . . . . . . 9 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
215125, 214sylan2 592 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
216215eximdv 1913 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
217124, 216mpd 15 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
218 df-rex 3067 . . . . . 6 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
219217, 218sylibr 233 . . . . 5 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
220219ralrimiva 3142 . . . 4 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
221 eqid 2728 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
222221fompt 7123 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
223114, 220, 222sylanbrc 582 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
224 fodomg 10540 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
2256, 223, 224sylc 65 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
226 domfi 9211 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2274, 225, 226syl2anc 583 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 846   = wceq 1534  wex 1774  [wsb 2060  wcel 2099  wne 2936  wral 3057  wrex 3066  ∃!wreu 3370  {crab 3428  Vcvv 3470  [wsbc 3775  csb 3890  cin 3944  wss 3945  c0 4319   cuni 4904  Disj wdisj 5108   class class class wbr 5143  cmpt 5226  ran crn 5674  ontowfo 6541  crio 7370  cdom 8956  Fincfn 8958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-ac2 10481
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-disj 5109  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7866  df-1st 7988  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-1o 8481  df-er 8719  df-map 8841  df-en 8959  df-dom 8960  df-fin 8962  df-card 9957  df-acn 9960  df-ac 10134
This theorem is referenced by:  fsumiunss  44954  sge0iunmptlemre  45794
  Copyright terms: Public domain W3C validator