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 39202
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 3832 . . . . 5 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
43a1i 11 . . . 4 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
5 ssfi 8177 . . . 4 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
62, 4, 5syl2anc 693 . . 3 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
71, 6syl 17 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
83a1i 11 . . . . 5 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
98, 1jca 554 . . . 4 (𝜑 → (( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin))
10 ssexg 4802 . . . 4 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
119, 10syl 17 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
12 elinel1 3797 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
13 eluni2 4438 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
1413biimpi 206 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
15 vex 3201 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
16 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5370 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1918biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
2019adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
21 nfcv 2763 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤
22 nfmpt1 4745 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
2322nfrn 5366 . . . . . . . . . . . . . . . . . . . . 21 𝑥ran (𝑥𝐴𝐵)
2421, 23nfel 2776 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
25 nfv 1842 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑦𝑤
2624, 25nfan 1827 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
27 simpl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
28 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2927, 28eleqtrd 2702 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
3029ex 450 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
3130a1d 25 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3231adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3326, 32reximdai 3011 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
3420, 33mpd 15 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
3534ex 450 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3635a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3736rexlimdv 3028 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3814, 37mpd 15 . . . . . . . . . . . . 13 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
3912, 38syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
4039adantl 482 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
41 nfv 1842 . . . . . . . . . . . . 13 𝑥𝜑
42 nfcv 2763 . . . . . . . . . . . . . 14 𝑥𝑦
4323nfuni 4440 . . . . . . . . . . . . . . 15 𝑥 ran (𝑥𝐴𝐵)
44 nfcv 2763 . . . . . . . . . . . . . . 15 𝑥𝐶
4543, 44nfin 3818 . . . . . . . . . . . . . 14 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
4642, 45nfel 2776 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
4741, 46nfan 1827 . . . . . . . . . . . 12 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
48 nfre1 3004 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
493sseli 3597 . . . . . . . . . . . . . 14 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
50 simp2 1061 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
51 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
52 simpl 473 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
5351, 52elind 3796 . . . . . . . . . . . . . . . . 17 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
54533adant2 1079 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
55 rspe 3002 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
5650, 54, 55syl2anc 693 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
57563exp 1263 . . . . . . . . . . . . . 14 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5849, 57syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5958adantl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
6047, 48, 59rexlimd 3024 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
6140, 60mpd 15 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
62 disjinfi.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑥𝐴 𝐵)
63 disjors 4633 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
6462, 63sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
65 nfv 1842 . . . . . . . . . . . . . . . . . . . . 21 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
66 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝐴
67 nfv 1842 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑧 = 𝑤
68 nfcsb1v 3547 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑧 / 𝑥𝐵
6921nfcsb1 3546 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑤 / 𝑥𝐵
7068, 69nfin 3818 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
71 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥
7270, 71nfeq 2775 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
7367, 72nfor 1833 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
7466, 73nfral 2944 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
75 equequ1 1951 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
76 csbeq1a 3540 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7776ineq1d 3811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
7877eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7975, 78orbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8079ralbidv 2985 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8165, 74, 80cbvral 3165 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
8264, 81sylibr 224 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
83 rspa 2929 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8482, 83sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8584adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
86 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → 𝑤𝐴)
87 rspa 2929 . . . . . . . . . . . . . . . . . 18 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8887orcomd 403 . . . . . . . . . . . . . . . . 17 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
8985, 86, 88syl2anc 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
9089adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
91 elinel1 3797 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
9291adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝐵)
93 sbsbc 3437 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
94 sbcel2 3987 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
95 csbin 4008 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
9695eleq2i 2692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9793, 94, 963bitri 286 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9897biimpi 206 . . . . . . . . . . . . . . . . . . . 20 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
99 elinel1 3797 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
101100adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
10292, 101jca 554 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → (𝑦𝐵𝑦𝑤 / 𝑥𝐵))
103 inelcm 4030 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
104103neneqd 2798 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
106105adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
107 pm2.53 388 . . . . . . . . . . . . . . 15 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
10890, 106, 107sylc 65 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → 𝑥 = 𝑤)
109108ex 450 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
110109ralrimiva 2965 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
111110ralrimiva 2965 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
112111adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
11361, 112jca 554 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
114 reu2 3392 . . . . . . . . 9 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
115113, 114sylibr 224 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
116 riotacl2 6621 . . . . . . . 8 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
117115, 116syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
118 nfriota1 6615 . . . . . . . . . . . 12 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
119118nfcsb1 3546 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
120119, 44nfin 3818 . . . . . . . . . . . . 13 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
12142, 120nfel 2776 . . . . . . . . . . . 12 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
122 csbeq1a 3540 . . . . . . . . . . . . . 14 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
123122ineq1d 3811 . . . . . . . . . . . . 13 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
124123eleq2d 2686 . . . . . . . . . . . 12 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
125118, 66, 121, 124elrabf 3358 . . . . . . . . . . 11 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
126125biimpi 206 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
127126simpld 475 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
128126simprd 479 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
129 ne0i 3919 . . . . . . . . . 10 (𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
130128, 129syl 17 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
131127, 130jca 554 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
132120, 71nfne 2893 . . . . . . . . 9 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
133123neeq1d 2852 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
134118, 66, 132, 133elrabf 3358 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
135131, 134sylibr 224 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
136117, 135syl 17 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
137136ralrimiva 2965 . . . . 5 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
13869, 44nfin 3818 . . . . . . . . . . . . 13 𝑥(𝑤 / 𝑥𝐵𝐶)
139138, 71nfne 2893 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
140 csbeq1a 3540 . . . . . . . . . . . . . 14 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
141140ineq1d 3811 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
142141neeq1d 2852 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
14321, 66, 139, 142elrabf 3358 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
144143simprbi 480 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
145 n0 3929 . . . . . . . . . 10 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
146144, 145sylib 208 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
147146adantl 482 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
148 nfv 1842 . . . . . . . . 9 𝑦(𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
149 simpl 473 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝜑)
150143simplbi 476 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
151150adantl 482 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝑤𝐴)
152 elinel1 3797 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
153152adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
154 simplr 792 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
155 nfv 1842 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑤𝐴)
156 nfcv 2763 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑉
15769, 156nfel 2776 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵𝑉
158155, 157nfim 1824 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
159 eleq1 2688 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
160159anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
161140eleq1d 2685 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
162160, 161imbi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
163 disjinfi.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵𝑉)
164158, 162, 163chvar 2261 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
165164adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
166 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
167166elrnmpt1 5372 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
168154, 165, 167syl2anc 693 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
169 nfcv 2763 . . . . . . . . . . . . . . . . 17 𝑤𝐵
170140equcoms 1946 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
171170eqcomd 2627 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
17269, 169, 171cbvmpt 4747 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
173172rneqi 5350 . . . . . . . . . . . . . . 15 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
174168, 173syl6eleq 2710 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
175 elunii 4439 . . . . . . . . . . . . . 14 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
176153, 174, 175syl2anc 693 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
177 elinel2 3798 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
178177adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
179176, 178elind 3796 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
180 nfv 1842 . . . . . . . . . . . . . . 15 𝑤 𝑦 ∈ (𝐵𝐶)
18142, 138nfel 2776 . . . . . . . . . . . . . . 15 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
182141eleq2d 2686 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
183180, 181, 182cbvriota 6618 . . . . . . . . . . . . . 14 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
184183a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
185 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
186154, 185jca 554 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
187 rspe 3002 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
188187adantll 750 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
189 simpll 790 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
190 sbequ 2375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
191 sbsbc 3437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
192191a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
193 sbcel2 3987 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
194 csbin 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
195 vex 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 ∈ V
196 csbconstg 3544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
197195, 196ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑧 / 𝑥𝐶 = 𝐶
198197ineq2i 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
199194, 198eqtri 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
200199eleq2i 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
201193, 200bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
202201a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
203190, 192, 2023bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
204203anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
205 equequ2 1952 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
206204, 205imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
207206cbvralv 3169 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
208207ralbii 2979 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
209 nfv 1842 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
21068, 44nfin 3818 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥(𝑧 / 𝑥𝐵𝐶)
21142, 210nfel 2776 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
212181, 211nfan 1827 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
213 nfv 1842 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑤 = 𝑧
214212, 213nfim 1824 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
21566, 214nfral 2944 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
216182anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
217 equequ1 1951 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
218216, 217imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
219218ralbidv 2985 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
220209, 215, 219cbvral 3165 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
221 biid 251 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
222 sbsbc 3437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
223 sbcel2 3987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
224 csbin 4008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
225 csbco 3541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
226 csbconstg 3544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
227195, 226ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝐶 = 𝐶
228225, 227ineq12i 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
229 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
230224, 228, 2293eqtri 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
231230eleq2i 2692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
232222, 223, 2313bitrri 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
233232anbi2i 730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
234233imbi1i 339 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
235234ralbii 2979 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
236235ralbii 2979 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
237221, 236bitri 264 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
238208, 220, 2373bitri 286 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
239112, 238sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
240189, 179, 239syl2anc 693 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
241188, 240jca 554 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
242 reu2 3392 . . . . . . . . . . . . . . . 16 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
243241, 242sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
244 riota1 6626 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
245243, 244syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
246186, 245mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
247184, 246eqtr2d 2656 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
248179, 247jca 554 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
249248ex 450 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
250149, 151, 249syl2anc 693 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
251148, 250eximd 2084 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
252147, 251mpd 15 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
253 df-rex 2917 . . . . . . 7 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
254252, 253sylibr 224 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
255254ralrimiva 2965 . . . . 5 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
256137, 255jca 554 . . . 4 (𝜑 → (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
257 eqid 2621 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
258257fompt 39201 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
259256, 258sylibr 224 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
260 fodomg 9342 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
26111, 259, 260sylc 65 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
262 domfi 8178 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2637, 261, 262syl2anc 693 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1037   = wceq 1482  wex 1703  [wsb 1879  wcel 1989  wne 2793  wral 2911  wrex 2912  ∃!wreu 2913  {crab 2915  Vcvv 3198  [wsbc 3433  csb 3531  cin 3571  wss 3572  c0 3913   cuni 4434  Disj wdisj 4618   class class class wbr 4651  cmpt 4727  ran crn 5113  ontowfo 5884  crio 6607  cdom 7950  Fincfn 7952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-ac2 9282
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-disj 4619  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-fin 7956  df-card 8762  df-acn 8765  df-ac 8936
This theorem is referenced by:  fsumiunss  39613  sge0iunmptlemre  40401
  Copyright terms: Public domain W3C validator