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 39694
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 3867 . . . . 5 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
43a1i 11 . . . 4 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
5 ssfi 8221 . . . 4 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
62, 4, 5syl2anc 694 . . 3 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
71, 6syl 17 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
83a1i 11 . . . . 5 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
98, 1jca 553 . . . 4 (𝜑 → (( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin))
10 ssexg 4837 . . . 4 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
119, 10syl 17 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
12 elinel1 3832 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
13 eluni2 4472 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
1413biimpi 206 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
15 vex 3234 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
16 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5404 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1918biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
2019adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
21 nfcv 2793 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤
22 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
2322nfrn 5400 . . . . . . . . . . . . . . . . . . . . 21 𝑥ran (𝑥𝐴𝐵)
2421, 23nfel 2806 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
25 nfv 1883 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑦𝑤
2624, 25nfan 1868 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
27 simpl 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
28 simpr 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2927, 28eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
3029ex 449 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
3130a1d 25 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3231adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3326, 32reximdai 3041 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
3420, 33mpd 15 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
3534ex 449 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3635a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3736rexlimdv 3059 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3814, 37mpd 15 . . . . . . . . . . . . 13 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
3912, 38syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
4039adantl 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
41 nfv 1883 . . . . . . . . . . . . 13 𝑥𝜑
42 nfcv 2793 . . . . . . . . . . . . . 14 𝑥𝑦
4323nfuni 4474 . . . . . . . . . . . . . . 15 𝑥 ran (𝑥𝐴𝐵)
44 nfcv 2793 . . . . . . . . . . . . . . 15 𝑥𝐶
4543, 44nfin 3853 . . . . . . . . . . . . . 14 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
4642, 45nfel 2806 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
4741, 46nfan 1868 . . . . . . . . . . . 12 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
48 nfre1 3034 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
493sseli 3632 . . . . . . . . . . . . . 14 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
50 simp2 1082 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
51 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
52 simpl 472 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
5351, 52elind 3831 . . . . . . . . . . . . . . . . 17 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
54533adant2 1100 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
55 rspe 3032 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
5650, 54, 55syl2anc 694 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
57563exp 1283 . . . . . . . . . . . . . 14 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5849, 57syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5958adantl 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
6047, 48, 59rexlimd 3055 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
6140, 60mpd 15 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
62 disjinfi.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑥𝐴 𝐵)
63 disjors 4667 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
6462, 63sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
65 nfv 1883 . . . . . . . . . . . . . . . . . . . . 21 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
66 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝐴
67 nfv 1883 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑧 = 𝑤
68 nfcsb1v 3582 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑧 / 𝑥𝐵
6921nfcsb1 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑤 / 𝑥𝐵
7068, 69nfin 3853 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
71 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥
7270, 71nfeq 2805 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
7367, 72nfor 1874 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
7466, 73nfral 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
75 equequ1 1998 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
76 csbeq1a 3575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7776ineq1d 3846 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
7877eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7975, 78orbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8079ralbidv 3015 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8165, 74, 80cbvral 3197 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
8264, 81sylibr 224 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
83 rspa 2959 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8482, 83sylan 487 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8584adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
86 simpr 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → 𝑤𝐴)
87 rspa 2959 . . . . . . . . . . . . . . . . . 18 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8887orcomd 402 . . . . . . . . . . . . . . . . 17 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
8985, 86, 88syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
9089adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
91 elinel1 3832 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
9291adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝐵)
93 sbsbc 3472 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
94 sbcel2 4022 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
95 csbin 4043 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
9695eleq2i 2722 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9793, 94, 963bitri 286 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9897biimpi 206 . . . . . . . . . . . . . . . . . . . 20 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
99 elinel1 3832 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
101100adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
10292, 101jca 553 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → (𝑦𝐵𝑦𝑤 / 𝑥𝐵))
103 inelcm 4065 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
104103neneqd 2828 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
106105adantl 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
107 pm2.53 387 . . . . . . . . . . . . . . 15 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
10890, 106, 107sylc 65 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → 𝑥 = 𝑤)
109108ex 449 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
110109ralrimiva 2995 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
111110ralrimiva 2995 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
112111adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
11361, 112jca 553 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
114 reu2 3427 . . . . . . . . 9 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
115113, 114sylibr 224 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
116 riotacl2 6664 . . . . . . . 8 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
117115, 116syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
118 nfriota1 6658 . . . . . . . . . . . 12 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
119118nfcsb1 3581 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
120119, 44nfin 3853 . . . . . . . . . . . . 13 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
12142, 120nfel 2806 . . . . . . . . . . . 12 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
122 csbeq1a 3575 . . . . . . . . . . . . . 14 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
123122ineq1d 3846 . . . . . . . . . . . . 13 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
124123eleq2d 2716 . . . . . . . . . . . 12 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
125118, 66, 121, 124elrabf 3392 . . . . . . . . . . 11 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
126125biimpi 206 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
127126simpld 474 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
128126simprd 478 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
129 ne0i 3954 . . . . . . . . . 10 (𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
130128, 129syl 17 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
131127, 130jca 553 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
132120, 71nfne 2923 . . . . . . . . 9 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
133123neeq1d 2882 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
134118, 66, 132, 133elrabf 3392 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
135131, 134sylibr 224 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
136117, 135syl 17 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
137136ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
13869, 44nfin 3853 . . . . . . . . . . . . 13 𝑥(𝑤 / 𝑥𝐵𝐶)
139138, 71nfne 2923 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
140 csbeq1a 3575 . . . . . . . . . . . . . 14 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
141140ineq1d 3846 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
142141neeq1d 2882 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
14321, 66, 139, 142elrabf 3392 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
144143simprbi 479 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
145 n0 3964 . . . . . . . . . 10 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
146144, 145sylib 208 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
147146adantl 481 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
148 nfv 1883 . . . . . . . . 9 𝑦(𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
149 simpl 472 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝜑)
150143simplbi 475 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
151150adantl 481 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝑤𝐴)
152 elinel1 3832 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
153152adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
154 simplr 807 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
155 nfv 1883 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑤𝐴)
156 nfcv 2793 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑉
15769, 156nfel 2806 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵𝑉
158155, 157nfim 1865 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
159 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
160159anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
161140eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
162160, 161imbi12d 333 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
163 disjinfi.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵𝑉)
164158, 162, 163chvar 2298 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
165164adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
166 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
167166elrnmpt1 5406 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
168154, 165, 167syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
169 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑤𝐵
170140equcoms 1993 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
171170eqcomd 2657 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
17269, 169, 171cbvmpt 4782 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
173172rneqi 5384 . . . . . . . . . . . . . . 15 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
174168, 173syl6eleq 2740 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
175 elunii 4473 . . . . . . . . . . . . . 14 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
176153, 174, 175syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
177 elinel2 3833 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
178177adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
179176, 178elind 3831 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
180 nfv 1883 . . . . . . . . . . . . . . 15 𝑤 𝑦 ∈ (𝐵𝐶)
18142, 138nfel 2806 . . . . . . . . . . . . . . 15 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
182141eleq2d 2716 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
183180, 181, 182cbvriota 6661 . . . . . . . . . . . . . 14 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
184183a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
185 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
186154, 185jca 553 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
187 rspe 3032 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
188187adantll 750 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
189 simpll 805 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
190 sbequ 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
191 sbsbc 3472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
192191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
193 sbcel2 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
194 csbin 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
195 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 ∈ V
196 csbconstg 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑧 / 𝑥𝐶 = 𝐶
198197ineq2i 3844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
199194, 198eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
200199eleq2i 2722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
201193, 200bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
202201a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
203190, 192, 2023bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
204203anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
205 equequ2 1999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
206204, 205imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
207206cbvralv 3201 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
208207ralbii 3009 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
209 nfv 1883 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
21068, 44nfin 3853 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥(𝑧 / 𝑥𝐵𝐶)
21142, 210nfel 2806 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
212181, 211nfan 1868 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
213 nfv 1883 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑤 = 𝑧
214212, 213nfim 1865 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
21566, 214nfral 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
216182anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
217 equequ1 1998 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
218216, 217imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
219218ralbidv 3015 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
220209, 215, 219cbvral 3197 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
221 biid 251 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
222 sbsbc 3472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
223 sbcel2 4022 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
224 csbin 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
225 csbco 3576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
226 csbconstg 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
227195, 226ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝐶 = 𝐶
228225, 227ineq12i 3845 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
229 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
230224, 228, 2293eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
231230eleq2i 2722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
232222, 223, 2313bitrri 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
233232anbi2i 730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
234233imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
235234ralbii 3009 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
236235ralbii 3009 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
237221, 236bitri 264 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
238208, 220, 2373bitri 286 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
239112, 238sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
240189, 179, 239syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
241188, 240jca 553 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
242 reu2 3427 . . . . . . . . . . . . . . . 16 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
243241, 242sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
244 riota1 6669 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
245243, 244syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
246186, 245mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
247184, 246eqtr2d 2686 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
248179, 247jca 553 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
249248ex 449 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
250149, 151, 249syl2anc 694 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
251148, 250eximd 2123 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
252147, 251mpd 15 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
253 df-rex 2947 . . . . . . 7 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
254252, 253sylibr 224 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
255254ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
256137, 255jca 553 . . . 4 (𝜑 → (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
257 eqid 2651 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
258257fompt 39693 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
259256, 258sylibr 224 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
260 fodomg 9383 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
26111, 259, 260sylc 65 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
262 domfi 8222 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2637, 261, 262syl2anc 694 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wex 1744  [wsb 1937  wcel 2030  wne 2823  wral 2941  wrex 2942  ∃!wreu 2943  {crab 2945  Vcvv 3231  [wsbc 3468  csb 3566  cin 3606  wss 3607  c0 3948   cuni 4468  Disj wdisj 4652   class class class wbr 4685  cmpt 4762  ran crn 5144  ontowfo 5924  crio 6650  cdom 7995  Fincfn 7997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-ac2 9323
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-fin 8001  df-card 8803  df-acn 8806  df-ac 8977
This theorem is referenced by:  fsumiunss  40125  sge0iunmptlemre  40950
  Copyright terms: Public domain W3C validator