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 39911
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 3989 . . . . 5 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
43a1i 11 . . . 4 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
5 ssfi 8357 . . . 4 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
62, 4, 5syl2anc 574 . . 3 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
71, 6syl 17 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
83a1i 11 . . . . 5 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
98, 1jca 502 . . . 4 (𝜑 → (( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin))
10 ssexg 4952 . . . 4 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
119, 10syl 17 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
12 elinel1 3957 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
13 eluni2 4589 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
1413biimpi 207 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
15 vex 3358 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
16 eqid 2774 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5522 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1918biimpi 207 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
2019adantr 467 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
21 nfcv 2916 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤
22 nfmpt1 4894 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
2322nfrn 5518 . . . . . . . . . . . . . . . . . . . . 21 𝑥ran (𝑥𝐴𝐵)
2421, 23nfel 2929 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
25 nfv 1998 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑦𝑤
2624, 25nfan 1983 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
27 simpl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
28 simpr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2927, 28eleqtrd 2855 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
3029ex 398 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
3130a1d 25 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3231adantl 468 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3326, 32reximdai 3163 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
3420, 33mpd 15 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
3534ex 398 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3635a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3736rexlimdv 3182 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3814, 37mpd 15 . . . . . . . . . . . . 13 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
3912, 38syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
4039adantl 468 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
41 nfv 1998 . . . . . . . . . . . . 13 𝑥𝜑
42 nfcv 2916 . . . . . . . . . . . . . 14 𝑥𝑦
4323nfuni 4591 . . . . . . . . . . . . . . 15 𝑥 ran (𝑥𝐴𝐵)
44 nfcv 2916 . . . . . . . . . . . . . . 15 𝑥𝐶
4543, 44nfin 3976 . . . . . . . . . . . . . 14 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
4642, 45nfel 2929 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
4741, 46nfan 1983 . . . . . . . . . . . 12 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
48 nfre1 3156 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
493sseli 3754 . . . . . . . . . . . . . 14 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
50 simp2 1158 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
51 simpr 472 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
52 simpl 469 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
5351, 52elind 3956 . . . . . . . . . . . . . . . . 17 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
54533adant2 1152 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
55 rspe 3154 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
5650, 54, 55syl2anc 574 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
57563exp 1139 . . . . . . . . . . . . . 14 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5849, 57syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5958adantl 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
6047, 48, 59rexlimd 3178 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
6140, 60mpd 15 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
62 disjinfi.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑥𝐴 𝐵)
63 disjors 4780 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
6462, 63sylib 209 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
65 nfv 1998 . . . . . . . . . . . . . . . . . . . . 21 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
66 nfcv 2916 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝐴
67 nfv 1998 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑧 = 𝑤
68 nfcsb1v 3704 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑧 / 𝑥𝐵
6921nfcsb1 3703 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑤 / 𝑥𝐵
7068, 69nfin 3976 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
71 nfcv 2916 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥
7270, 71nfeq 2928 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
7367, 72nfor 1989 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
7466, 73nfral 3097 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
75 equequ1 2113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
76 csbeq1a 3697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7776ineq1d 3971 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
7877eqeq1d 2776 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7975, 78orbi12d 931 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8079ralbidv 3138 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8165, 74, 80cbvral 3320 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
8264, 81sylibr 225 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
83 rspa 3082 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8482, 83sylan 570 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8584adantr 467 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
86 simpr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → 𝑤𝐴)
87 rspa 3082 . . . . . . . . . . . . . . . . . 18 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8887orcomd 887 . . . . . . . . . . . . . . . . 17 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
8985, 86, 88syl2anc 574 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
9089adantr 467 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
91 elinel1 3957 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
9291adantr 467 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝐵)
93 sbsbc 3597 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
94 sbcel2 4143 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
95 csbin 4164 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
9695eleq2i 2845 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9793, 94, 963bitri 287 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9897biimpi 207 . . . . . . . . . . . . . . . . . . . 20 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
99 elinel1 3957 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
101100adantl 468 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
10292, 101jca 502 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → (𝑦𝐵𝑦𝑤 / 𝑥𝐵))
103 inelcm 4185 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
104103neneqd 2951 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
106105adantl 468 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
107 pm2.53 867 . . . . . . . . . . . . . . 15 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
10890, 106, 107sylc 65 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → 𝑥 = 𝑤)
109108ex 398 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
110109ralrimiva 3118 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
111110ralrimiva 3118 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
112111adantr 467 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
11361, 112jca 502 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
114 reu2 3552 . . . . . . . . 9 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
115113, 114sylibr 225 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
116 riotacl2 6786 . . . . . . . 8 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
117115, 116syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
118 nfriota1 6780 . . . . . . . . . . . 12 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
119118nfcsb1 3703 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
120119, 44nfin 3976 . . . . . . . . . . . . 13 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
12142, 120nfel 2929 . . . . . . . . . . . 12 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
122 csbeq1a 3697 . . . . . . . . . . . . . 14 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
123122ineq1d 3971 . . . . . . . . . . . . 13 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
124123eleq2d 2839 . . . . . . . . . . . 12 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
125118, 66, 121, 124elrabf 3517 . . . . . . . . . . 11 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
126125biimpi 207 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
127126simpld 483 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
128126simprd 484 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
129128ne0d 4080 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
130127, 129jca 502 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
131120, 71nfne 3046 . . . . . . . . 9 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
132123neeq1d 3005 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
133118, 66, 131, 132elrabf 3517 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
134130, 133sylibr 225 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
135117, 134syl 17 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
136135ralrimiva 3118 . . . . 5 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
13769, 44nfin 3976 . . . . . . . . . . . . 13 𝑥(𝑤 / 𝑥𝐵𝐶)
138137, 71nfne 3046 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
139 csbeq1a 3697 . . . . . . . . . . . . . 14 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
140139ineq1d 3971 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
141140neeq1d 3005 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
14221, 66, 138, 141elrabf 3517 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
143142simprbi 485 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
144 n0 4089 . . . . . . . . . 10 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
145143, 144sylib 209 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
146145adantl 468 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
147 nfv 1998 . . . . . . . . 9 𝑦(𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
148 simpl 469 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝜑)
149142simplbi 486 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
150149adantl 468 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝑤𝐴)
151 elinel1 3957 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
152151adantl 468 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
153 simplr 774 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
154 nfv 1998 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑤𝐴)
155 nfcv 2916 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑉
15669, 155nfel 2929 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵𝑉
157154, 156nfim 1980 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
158 eleq1w 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
159158anbi2d 615 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
160139eleq1d 2838 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
161159, 160imbi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
162 disjinfi.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵𝑉)
163157, 161, 162chvar 2427 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
164163adantr 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
165 eqid 2774 . . . . . . . . . . . . . . . . 17 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
166165elrnmpt1 5524 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
167153, 164, 166syl2anc 574 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
168 nfcv 2916 . . . . . . . . . . . . . . . . 17 𝑤𝐵
169139equcoms 2108 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
170169eqcomd 2780 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
17169, 168, 170cbvmpt 4896 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
172171rneqi 5502 . . . . . . . . . . . . . . 15 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
173167, 172syl6eleq 2863 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
174 elunii 4590 . . . . . . . . . . . . . 14 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
175152, 173, 174syl2anc 574 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
176 elinel2 3958 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
177176adantl 468 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
178175, 177elind 3956 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
179 nfv 1998 . . . . . . . . . . . . . . 15 𝑤 𝑦 ∈ (𝐵𝐶)
18042, 137nfel 2929 . . . . . . . . . . . . . . 15 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
181140eleq2d 2839 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
182179, 180, 181cbvriota 6783 . . . . . . . . . . . . . 14 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
184 simpr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
185153, 184jca 502 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
186 rspe 3154 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
187186adantll 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
188 simpll 772 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
189 sbequ 2526 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
190 sbsbc 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
191190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
192 sbcel2 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
193 csbin 4164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
194 vex 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 ∈ V
195 csbconstg 3701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
196194, 195ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑧 / 𝑥𝐶 = 𝐶
197196ineq2i 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
198193, 197eqtri 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
199198eleq2i 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
200192, 199bitri 265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
202189, 191, 2013bitrd 295 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
203202anbi2d 615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
204 equequ2 2114 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
205203, 204imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
206205cbvralv 3324 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
207206ralbii 3132 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
208 nfv 1998 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
20968, 44nfin 3976 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥(𝑧 / 𝑥𝐵𝐶)
21042, 209nfel 2929 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
211180, 210nfan 1983 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
212 nfv 1998 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑤 = 𝑧
213211, 212nfim 1980 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
21466, 213nfral 3097 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
215181anbi1d 616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
216 equequ1 2113 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
217215, 216imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
218217ralbidv 3138 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
219208, 214, 218cbvral 3320 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
220 biid 252 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
221 sbsbc 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
222 sbcel2 4143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
223 csbin 4164 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
224 csbco 3698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
225 csbconstg 3701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
226194, 225ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝐶 = 𝐶
227224, 226ineq12i 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
228 eqid 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
229223, 227, 2283eqtri 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
230229eleq2i 2845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
231221, 222, 2303bitrri 288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
232231anbi2i 610 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
233232imbi1i 339 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
234233ralbii 3132 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
235234ralbii 3132 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
236220, 235bitri 265 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
237207, 219, 2363bitri 287 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
238112, 237sylib 209 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
239188, 178, 238syl2anc 574 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
240187, 239jca 502 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
241 reu2 3552 . . . . . . . . . . . . . . . 16 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
242240, 241sylibr 225 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
243 riota1 6791 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
244242, 243syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
245185, 244mpbid 223 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
246183, 245eqtr2d 2809 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
247178, 246jca 502 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
248247ex 398 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
249148, 150, 248syl2anc 574 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
250147, 249eximd 2244 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
251146, 250mpd 15 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
252 df-rex 3070 . . . . . . 7 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
253251, 252sylibr 225 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
254253ralrimiva 3118 . . . . 5 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
255136, 254jca 502 . . . 4 (𝜑 → (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
256 eqid 2774 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
257256fompt 39910 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
258255, 257sylibr 225 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
259 fodomg 9568 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
26011, 258, 259sylc 65 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
261 domfi 8358 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2627, 260, 261syl2anc 574 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  wo 863  w3a 1098   = wceq 1634  wex 1855  [wsb 2052  wcel 2148  wne 2946  wral 3064  wrex 3065  ∃!wreu 3066  {crab 3068  Vcvv 3355  [wsbc 3593  csb 3688  cin 3728  wss 3729  c0 4073   cuni 4585  Disj wdisj 4765   class class class wbr 4797  cmpt 4876  ran crn 5264  ontowfo 6040  crio 6772  cdom 8128  Fincfn 8130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-ac2 9508
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-disj 4766  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-er 7917  df-map 8032  df-en 8131  df-dom 8132  df-fin 8134  df-card 8986  df-acn 8989  df-ac 9160
This theorem is referenced by:  fsumiunss  40331  sge0iunmptlemre  41155
  Copyright terms: Public domain W3C validator