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 38175
Description: Only a finite number of disjoint sets can have a non empty 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 id 22 . . . 4 (𝐶 ∈ Fin → 𝐶 ∈ Fin)
3 inss2 3792 . . . . 5 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
43a1i 11 . . . 4 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
5 ssfi 8039 . . . 4 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
62, 4, 5syl2anc 690 . . 3 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
71, 6syl 17 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
83a1i 11 . . . . 5 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
98, 1jca 552 . . . 4 (𝜑 → (( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin))
10 ssexg 4724 . . . 4 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
119, 10syl 17 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
12 elinel1 3757 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
13 eluni2 4367 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
1413biimpi 204 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
15 vex 3172 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
16 eqid 2606 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5277 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1918biimpi 204 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
2019adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
21 nfcv 2747 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤
22 nfmpt1 4666 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
2322nfrn 5273 . . . . . . . . . . . . . . . . . . . . 21 𝑥ran (𝑥𝐴𝐵)
2421, 23nfel 2759 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
25 nfv 1829 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑦𝑤
2624, 25nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
27 simpl 471 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
28 simpr 475 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2927, 28eleqtrd 2686 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
3029ex 448 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
3130a1d 25 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3231adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3326, 32reximdai 2991 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
3420, 33mpd 15 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
3534ex 448 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3635a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3736rexlimdv 3008 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3814, 37mpd 15 . . . . . . . . . . . . 13 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
3912, 38syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
4039adantl 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
41 nfv 1829 . . . . . . . . . . . . 13 𝑥𝜑
42 nfcv 2747 . . . . . . . . . . . . . 14 𝑥𝑦
4323nfuni 4369 . . . . . . . . . . . . . . 15 𝑥 ran (𝑥𝐴𝐵)
44 nfcv 2747 . . . . . . . . . . . . . . 15 𝑥𝐶
4543, 44nfin 3778 . . . . . . . . . . . . . 14 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
4642, 45nfel 2759 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
4741, 46nfan 1815 . . . . . . . . . . . 12 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
48 nfre1 2984 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
493sseli 3560 . . . . . . . . . . . . . 14 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
50 simp2 1054 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
51 simpr 475 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
52 simpl 471 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
5351, 52elind 3756 . . . . . . . . . . . . . . . . 17 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
54533adant2 1072 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
55 rspe 2982 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
5650, 54, 55syl2anc 690 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
57563exp 1255 . . . . . . . . . . . . . 14 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5849, 57syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5958adantl 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
6047, 48, 59rexlimd 3004 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
6140, 60mpd 15 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
62 disjinfi.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑥𝐴 𝐵)
63 disjors 4559 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
6462, 63sylib 206 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
65 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
66 nfcv 2747 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝐴
67 nfv 1829 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑧 = 𝑤
68 nfcsb1v 3511 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑧 / 𝑥𝐵
6921nfcsb1 3510 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑤 / 𝑥𝐵
7068, 69nfin 3778 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
71 nfcv 2747 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥
7270, 71nfeq 2758 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
7367, 72nfor 1821 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
7466, 73nfral 2925 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
75 equequ1 1938 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
76 csbeq1a 3504 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7776ineq1d 3771 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
7877eqeq1d 2608 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7975, 78orbi12d 741 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8079ralbidv 2965 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8165, 74, 80cbvral 3139 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
8264, 81sylibr 222 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
83 rspa 2910 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8482, 83sylan 486 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8584adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
86 simpr 475 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → 𝑤𝐴)
87 rspa 2910 . . . . . . . . . . . . . . . . . 18 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8887orcomd 401 . . . . . . . . . . . . . . . . 17 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
8985, 86, 88syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
9089adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
91 elinel1 3757 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
9291adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝐵)
93 sbsbc 3402 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
94 sbcel2 3937 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
95 csbin 3958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
9695eleq2i 2676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9793, 94, 963bitri 284 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9897biimpi 204 . . . . . . . . . . . . . . . . . . . 20 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
99 elinel1 3757 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
101100adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
10292, 101jca 552 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → (𝑦𝐵𝑦𝑤 / 𝑥𝐵))
103 inelcm 3980 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
104103neneqd 2783 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
106105adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
107 pm2.53 386 . . . . . . . . . . . . . . 15 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
10890, 106, 107sylc 62 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → 𝑥 = 𝑤)
109108ex 448 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
110109ralrimiva 2945 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
111110ralrimiva 2945 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
112111adantr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
11361, 112jca 552 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
114 reu2 3357 . . . . . . . . 9 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
115113, 114sylibr 222 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
116 riotacl2 6499 . . . . . . . 8 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
117115, 116syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
118 nfriota1 6493 . . . . . . . . . . . 12 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
119118nfcsb1 3510 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
120119, 44nfin 3778 . . . . . . . . . . . . 13 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
12142, 120nfel 2759 . . . . . . . . . . . 12 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
122 csbeq1a 3504 . . . . . . . . . . . . . 14 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
123122ineq1d 3771 . . . . . . . . . . . . 13 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
124123eleq2d 2669 . . . . . . . . . . . 12 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
125118, 66, 121, 124elrabf 3325 . . . . . . . . . . 11 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
126125biimpi 204 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
127126simpld 473 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
128126simprd 477 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
129 ne0i 3876 . . . . . . . . . 10 (𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
130128, 129syl 17 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
131127, 130jca 552 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
132120, 71nfne 2878 . . . . . . . . 9 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
133123neeq1d 2837 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
134118, 66, 132, 133elrabf 3325 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
135131, 134sylibr 222 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
136117, 135syl 17 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
137136ralrimiva 2945 . . . . 5 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
13869, 44nfin 3778 . . . . . . . . . . . . 13 𝑥(𝑤 / 𝑥𝐵𝐶)
139138, 71nfne 2878 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
140 csbeq1a 3504 . . . . . . . . . . . . . 14 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
141140ineq1d 3771 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
142141neeq1d 2837 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
14321, 66, 139, 142elrabf 3325 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
144143simprbi 478 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
145 n0 3886 . . . . . . . . . 10 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
146144, 145sylib 206 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
147146adantl 480 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
148 nfv 1829 . . . . . . . . 9 𝑦(𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
149 simpl 471 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝜑)
150143simplbi 474 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
151150adantl 480 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝑤𝐴)
152 elinel1 3757 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
153152adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
154 simplr 787 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
155 nfv 1829 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑤𝐴)
156 nfcv 2747 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑉
15769, 156nfel 2759 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵𝑉
158155, 157nfim 1812 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
159 eleq1 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
160159anbi2d 735 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
161140eleq1d 2668 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
162160, 161imbi12d 332 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
163 disjinfi.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵𝑉)
164158, 162, 163chvar 2245 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
165164adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
166 eqid 2606 . . . . . . . . . . . . . . . . 17 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
167166elrnmpt1 5279 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
168154, 165, 167syl2anc 690 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
169 nfcv 2747 . . . . . . . . . . . . . . . . 17 𝑤𝐵
170140equcoms 1933 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
171170eqcomd 2612 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
17269, 169, 171cbvmpt 4668 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
173172rneqi 5257 . . . . . . . . . . . . . . 15 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
174168, 173syl6eleq 2694 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
175 elunii 4368 . . . . . . . . . . . . . 14 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
176153, 174, 175syl2anc 690 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
177 elinel2 3758 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
178177adantl 480 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
179176, 178elind 3756 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
180 nfv 1829 . . . . . . . . . . . . . . 15 𝑤 𝑦 ∈ (𝐵𝐶)
18142, 138nfel 2759 . . . . . . . . . . . . . . 15 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
182141eleq2d 2669 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
183180, 181, 182cbvriota 6496 . . . . . . . . . . . . . 14 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
184183a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
185 simpr 475 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
186154, 185jca 552 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
187 rspe 2982 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
188187adantll 745 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
189 simpll 785 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
190 sbequ 2360 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
191 sbsbc 3402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
192191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
193 sbcel2 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
194 csbin 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
195 vex 3172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 ∈ V
196 csbconstg 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑧 / 𝑥𝐶 = 𝐶
198197ineq2i 3769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
199194, 198eqtri 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
200199eleq2i 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
201193, 200bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
202201a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
203190, 192, 2023bitrd 292 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
204203anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
205 equequ2 1939 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
206204, 205imbi12d 332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
207206cbvralv 3143 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
208207ralbii 2959 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
209 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
21068, 44nfin 3778 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥(𝑧 / 𝑥𝐵𝐶)
21142, 210nfel 2759 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
212181, 211nfan 1815 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
213 nfv 1829 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑤 = 𝑧
214212, 213nfim 1812 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
21566, 214nfral 2925 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
216182anbi1d 736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
217 equequ1 1938 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
218216, 217imbi12d 332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
219218ralbidv 2965 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
220209, 215, 219cbvral 3139 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
221 biid 249 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
222 sbsbc 3402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
223 sbcel2 3937 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
224 csbin 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
225 csbco 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
226 csbconstg 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
227195, 226ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝐶 = 𝐶
228225, 227ineq12i 3770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
229 eqid 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
230224, 228, 2293eqtri 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
231230eleq2i 2676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
232222, 223, 2313bitrri 285 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
233232anbi2i 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
234233imbi1i 337 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
235234ralbii 2959 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
236235ralbii 2959 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
237221, 236bitri 262 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
238208, 220, 2373bitri 284 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
239112, 238sylib 206 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
240189, 179, 239syl2anc 690 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
241188, 240jca 552 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
242 reu2 3357 . . . . . . . . . . . . . . . 16 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
243241, 242sylibr 222 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
244 riota1 6504 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
245243, 244syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
246186, 245mpbid 220 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
247184, 246eqtr2d 2641 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
248179, 247jca 552 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
249248ex 448 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
250149, 151, 249syl2anc 690 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
251148, 250eximd 2070 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
252147, 251mpd 15 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
253 df-rex 2898 . . . . . . 7 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
254252, 253sylibr 222 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
255254ralrimiva 2945 . . . . 5 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
256137, 255jca 552 . . . 4 (𝜑 → (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
257 eqid 2606 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
258257fompt 38174 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
259256, 258sylibr 222 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
260 fodomg 9202 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
26111, 259, 260sylc 62 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
262 domfi 8040 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2637, 261, 262syl2anc 690 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wex 1694  [wsb 1866  wcel 1976  wne 2776  wral 2892  wrex 2893  ∃!wreu 2894  {crab 2896  Vcvv 3169  [wsbc 3398  csb 3495  cin 3535  wss 3536  c0 3870   cuni 4363  Disj wdisj 4544   class class class wbr 4574  cmpt 4634  ran crn 5026  ontowfo 5785  crio 6485  cdom 7813  Fincfn 7815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-ac2 9142
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-disj 4545  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-er 7603  df-map 7720  df-en 7816  df-dom 7817  df-fin 7819  df-card 8622  df-acn 8625  df-ac 8796
This theorem is referenced by:  fsumiunss  38443  sge0iunmptlemre  39109
  Copyright terms: Public domain W3C validator