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 40187
Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶 (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
disjinfi.b ((𝜑𝑥𝐴) → 𝐵𝑉)
disjinfi.d (𝜑Disj 𝑥𝐴 𝐵)
disjinfi.c (𝜑𝐶 ∈ Fin)
Assertion
Ref Expression
disjinfi (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝑉   𝜑,𝑥
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem disjinfi
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjinfi.c . . 3 (𝜑𝐶 ∈ Fin)
2 id 22 . . . 4 (𝐶 ∈ Fin → 𝐶 ∈ Fin)
3 inss2 4057 . . . . 5 ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶
43a1i 11 . . . 4 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
5 ssfi 8448 . . . 4 ((𝐶 ∈ Fin ∧ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
62, 4, 5syl2anc 581 . . 3 (𝐶 ∈ Fin → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
71, 6syl 17 . 2 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin)
83a1i 11 . . . . 5 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶)
98, 1jca 509 . . . 4 (𝜑 → (( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin))
10 ssexg 5028 . . . 4 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ⊆ 𝐶𝐶 ∈ Fin) → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
119, 10syl 17 . . 3 (𝜑 → ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V)
12 elinel1 4025 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦 ran (𝑥𝐴𝐵))
13 eluni2 4661 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) ↔ ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
1413biimpi 208 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤)
15 vex 3416 . . . . . . . . . . . . . . . . . . . . 21 𝑤 ∈ V
16 eqid 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
1716elrnmpt 5604 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ V → (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵))
1815, 17ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ran (𝑥𝐴𝐵) ↔ ∃𝑥𝐴 𝑤 = 𝐵)
1918biimpi 208 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑤 = 𝐵)
2019adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑤 = 𝐵)
21 nfcv 2968 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤
22 nfmpt1 4969 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑥𝐴𝐵)
2322nfrn 5600 . . . . . . . . . . . . . . . . . . . . 21 𝑥ran (𝑥𝐴𝐵)
2421, 23nfel 2981 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑤 ∈ ran (𝑥𝐴𝐵)
25 nfv 2015 . . . . . . . . . . . . . . . . . . . 20 𝑥 𝑦𝑤
2624, 25nfan 2004 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤)
27 simpl 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝑤)
28 simpr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝑤𝑤 = 𝐵) → 𝑤 = 𝐵)
2927, 28eleqtrd 2907 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝑤𝑤 = 𝐵) → 𝑦𝐵)
3029ex 403 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑤 → (𝑤 = 𝐵𝑦𝐵))
3130a1d 25 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑤 → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3231adantl 475 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (𝑥𝐴 → (𝑤 = 𝐵𝑦𝐵)))
3326, 32reximdai 3219 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → (∃𝑥𝐴 𝑤 = 𝐵 → ∃𝑥𝐴 𝑦𝐵))
3420, 33mpd 15 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ran (𝑥𝐴𝐵) ∧ 𝑦𝑤) → ∃𝑥𝐴 𝑦𝐵)
3534ex 403 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3635a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ran (𝑥𝐴𝐵) → (𝑤 ∈ ran (𝑥𝐴𝐵) → (𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵)))
3736rexlimdv 3238 . . . . . . . . . . . . . 14 (𝑦 ran (𝑥𝐴𝐵) → (∃𝑤 ∈ ran (𝑥𝐴𝐵)𝑦𝑤 → ∃𝑥𝐴 𝑦𝐵))
3814, 37mpd 15 . . . . . . . . . . . . 13 (𝑦 ran (𝑥𝐴𝐵) → ∃𝑥𝐴 𝑦𝐵)
3912, 38syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → ∃𝑥𝐴 𝑦𝐵)
4039adantl 475 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦𝐵)
41 nfv 2015 . . . . . . . . . . . . 13 𝑥𝜑
42 nfcv 2968 . . . . . . . . . . . . . 14 𝑥𝑦
4323nfuni 4663 . . . . . . . . . . . . . . 15 𝑥 ran (𝑥𝐴𝐵)
44 nfcv 2968 . . . . . . . . . . . . . . 15 𝑥𝐶
4543, 44nfin 4044 . . . . . . . . . . . . . 14 𝑥( ran (𝑥𝐴𝐵) ∩ 𝐶)
4642, 45nfel 2981 . . . . . . . . . . . . 13 𝑥 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)
4741, 46nfan 2004 . . . . . . . . . . . 12 𝑥(𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
48 nfre1 3212 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑦 ∈ (𝐵𝐶)
493sseli 3822 . . . . . . . . . . . . . 14 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → 𝑦𝐶)
50 simp2 1173 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑥𝐴)
51 simpr 479 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐵)
52 simpl 476 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐶𝑦𝐵) → 𝑦𝐶)
5351, 52elind 4024 . . . . . . . . . . . . . . . . 17 ((𝑦𝐶𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
54533adant2 1167 . . . . . . . . . . . . . . . 16 ((𝑦𝐶𝑥𝐴𝑦𝐵) → 𝑦 ∈ (𝐵𝐶))
55 rspe 3210 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦 ∈ (𝐵𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
5650, 54, 55syl2anc 581 . . . . . . . . . . . . . . 15 ((𝑦𝐶𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
57563exp 1154 . . . . . . . . . . . . . 14 (𝑦𝐶 → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5849, 57syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
5958adantl 475 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
6047, 48, 59rexlimd 3234 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦𝐵 → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
6140, 60mpd 15 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
62 disjinfi.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑥𝐴 𝐵)
63 disjors 4855 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
6462, 63sylib 210 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
65 nfv 2015 . . . . . . . . . . . . . . . . . . . . 21 𝑧𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅)
66 nfcv 2968 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝐴
67 nfv 2015 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑧 = 𝑤
68 nfcsb1v 3772 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑧 / 𝑥𝐵
6921nfcsb1 3771 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝑤 / 𝑥𝐵
7068, 69nfin 4044 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵)
71 nfcv 2968 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥
7270, 71nfeq 2980 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅
7367, 72nfor 2009 . . . . . . . . . . . . . . . . . . . . . 22 𝑥(𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
7466, 73nfral 3153 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)
75 equequ1 2131 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
76 csbeq1a 3765 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7776ineq1d 4039 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → (𝐵𝑤 / 𝑥𝐵) = (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵))
7877eqeq1d 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → ((𝐵𝑤 / 𝑥𝐵) = ∅ ↔ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
7975, 78orbi12d 949 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8079ralbidv 3194 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅)))
8165, 74, 80cbvral 3378 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ↔ ∀𝑧𝐴𝑤𝐴 (𝑧 = 𝑤 ∨ (𝑧 / 𝑥𝐵𝑤 / 𝑥𝐵) = ∅))
8264, 81sylibr 226 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
83 rspa 3138 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝐴𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8482, 83sylan 577 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8584adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
86 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → 𝑤𝐴)
87 rspa 3138 . . . . . . . . . . . . . . . . . 18 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅))
8887orcomd 904 . . . . . . . . . . . . . . . . 17 ((∀𝑤𝐴 (𝑥 = 𝑤 ∨ (𝐵𝑤 / 𝑥𝐵) = ∅) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
8985, 86, 88syl2anc 581 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
9089adantr 474 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤))
91 elinel1 4025 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝐵𝐶) → 𝑦𝐵)
9291adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝐵)
93 sbsbc 3665 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))
94 sbcel2 4212 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑤 / 𝑥(𝐵𝐶))
95 csbin 4234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 / 𝑥(𝐵𝐶) = (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶)
9695eleq2i 2897 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑤 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9793, 94, 963bitri 289 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
9897biimpi 208 . . . . . . . . . . . . . . . . . . . 20 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶))
99 elinel1 4025 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑤 / 𝑥𝐵𝑤 / 𝑥𝐶) → 𝑦𝑤 / 𝑥𝐵)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . 19 ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
101100adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
10292, 101jca 509 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → (𝑦𝐵𝑦𝑤 / 𝑥𝐵))
103 inelcm 4255 . . . . . . . . . . . . . . . . . 18 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → (𝐵𝑤 / 𝑥𝐵) ≠ ∅)
104103neneqd 3003 . . . . . . . . . . . . . . . . 17 ((𝑦𝐵𝑦𝑤 / 𝑥𝐵) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
106105adantl 475 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → ¬ (𝐵𝑤 / 𝑥𝐵) = ∅)
107 pm2.53 884 . . . . . . . . . . . . . . 15 (((𝐵𝑤 / 𝑥𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵𝑤 / 𝑥𝐵) = ∅ → 𝑥 = 𝑤))
10890, 106, 107sylc 65 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐴) ∧ 𝑤𝐴) ∧ (𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶))) → 𝑥 = 𝑤)
109108ex 403 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑤𝐴) → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
110109ralrimiva 3174 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
111110ralrimiva 3174 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
112111adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤))
11361, 112jca 509 . . . . . . . . 9 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
114 reu2 3618 . . . . . . . . 9 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ∧ ∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤)))
115113, 114sylibr 226 . . . . . . . 8 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶))
116 riotacl2 6878 . . . . . . . 8 (∃!𝑥𝐴 𝑦 ∈ (𝐵𝐶) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
117115, 116syl 17 . . . . . . 7 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)})
118 nfriota1 6872 . . . . . . . . . . . 12 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶))
119118nfcsb1 3771 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵
120119, 44nfin 4044 . . . . . . . . . . . . 13 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
12142, 120nfel 2981 . . . . . . . . . . . 12 𝑥 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)
122 csbeq1a 3765 . . . . . . . . . . . . . 14 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → 𝐵 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵)
123122ineq1d 4039 . . . . . . . . . . . . 13 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝐵𝐶) = ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
124123eleq2d 2891 . . . . . . . . . . . 12 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
125118, 66, 121, 124elrabf 3580 . . . . . . . . . . 11 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
126125biimpi 208 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶)))
127126simpld 490 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴)
128126simprd 491 . . . . . . . . . 10 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → 𝑦 ∈ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶))
129128ne0d 4150 . . . . . . . . 9 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅)
130127, 129jca 509 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
131120, 71nfne 3098 . . . . . . . . 9 𝑥((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅
132123neeq1d 3057 . . . . . . . . 9 (𝑥 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) → ((𝐵𝐶) ≠ ∅ ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
133118, 66, 131, 132elrabf 3580 . . . . . . . 8 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ 𝐴 ∧ ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) / 𝑥𝐵𝐶) ≠ ∅))
134130, 133sylibr 226 . . . . . . 7 ((𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴𝑦 ∈ (𝐵𝐶)} → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
135117, 134syl 17 . . . . . 6 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
136135ralrimiva 3174 . . . . 5 (𝜑 → ∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
13769, 44nfin 4044 . . . . . . . . . . . . 13 𝑥(𝑤 / 𝑥𝐵𝐶)
138137, 71nfne 3098 . . . . . . . . . . . 12 𝑥(𝑤 / 𝑥𝐵𝐶) ≠ ∅
139 csbeq1a 3765 . . . . . . . . . . . . . 14 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
140139ineq1d 4039 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵𝐶) = (𝑤 / 𝑥𝐵𝐶))
141140neeq1d 3057 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐵𝐶) ≠ ∅ ↔ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
14221, 66, 138, 141elrabf 3580 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (𝑤𝐴 ∧ (𝑤 / 𝑥𝐵𝐶) ≠ ∅))
143142simprbi 492 . . . . . . . . . 10 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → (𝑤 / 𝑥𝐵𝐶) ≠ ∅)
144 n0 4159 . . . . . . . . . 10 ((𝑤 / 𝑥𝐵𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
145143, 144sylib 210 . . . . . . . . 9 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
146145adantl 475 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
147 nfv 2015 . . . . . . . . 9 𝑦(𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
148 simpl 476 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝜑)
149142simplbi 493 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → 𝑤𝐴)
150149adantl 475 . . . . . . . . . 10 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → 𝑤𝐴)
151 elinel1 4025 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝑤 / 𝑥𝐵)
152151adantl 475 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝑤 / 𝑥𝐵)
153 simplr 787 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤𝐴)
154 nfv 2015 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑𝑤𝐴)
155 nfcv 2968 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑉
15669, 155nfel 2981 . . . . . . . . . . . . . . . . . . 19 𝑥𝑤 / 𝑥𝐵𝑉
157154, 156nfim 2001 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
158 eleq1w 2888 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
159158anbi2d 624 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
160139eleq1d 2890 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → (𝐵𝑉𝑤 / 𝑥𝐵𝑉))
161159, 160imbi12d 336 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → 𝐵𝑉) ↔ ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)))
162 disjinfi.b . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → 𝐵𝑉)
163157, 161, 162chvar 2415 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝐴) → 𝑤 / 𝑥𝐵𝑉)
164163adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵𝑉)
165 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑤𝐴𝑤 / 𝑥𝐵)
166165elrnmpt1 5606 . . . . . . . . . . . . . . . 16 ((𝑤𝐴𝑤 / 𝑥𝐵𝑉) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
167153, 164, 166syl2anc 581 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑤𝐴𝑤 / 𝑥𝐵))
168 nfcv 2968 . . . . . . . . . . . . . . . . 17 𝑤𝐵
169139equcoms 2126 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥𝐵 = 𝑤 / 𝑥𝐵)
170169eqcomd 2830 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥𝑤 / 𝑥𝐵 = 𝐵)
17169, 168, 170cbvmpt 4971 . . . . . . . . . . . . . . . 16 (𝑤𝐴𝑤 / 𝑥𝐵) = (𝑥𝐴𝐵)
172171rneqi 5583 . . . . . . . . . . . . . . 15 ran (𝑤𝐴𝑤 / 𝑥𝐵) = ran (𝑥𝐴𝐵)
173167, 172syl6eleq 2915 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵))
174 elunii 4662 . . . . . . . . . . . . . 14 ((𝑦𝑤 / 𝑥𝐵𝑤 / 𝑥𝐵 ∈ ran (𝑥𝐴𝐵)) → 𝑦 ran (𝑥𝐴𝐵))
175152, 173, 174syl2anc 581 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ran (𝑥𝐴𝐵))
176 elinel2 4026 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → 𝑦𝐶)
177176adantl 475 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦𝐶)
178175, 177elind 4024 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
179 nfv 2015 . . . . . . . . . . . . . . 15 𝑤 𝑦 ∈ (𝐵𝐶)
18042, 137nfel 2981 . . . . . . . . . . . . . . 15 𝑥 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)
181140eleq2d 2891 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
182179, 180, 181cbvriota 6875 . . . . . . . . . . . . . 14 (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) = (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
184 simpr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
185153, 184jca 509 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
186 rspe 3210 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
187186adantll 707 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
188 simpll 785 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝜑)
189 sbequ 2506 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
190 sbsbc 3665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶))
191190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶)))
192 sbcel2 4212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦𝑧 / 𝑥(𝐵𝐶))
193 csbin 4234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶)
194 vex 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 ∈ V
195 csbconstg 3769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ V → 𝑧 / 𝑥𝐶 = 𝐶)
196194, 195ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑧 / 𝑥𝐶 = 𝐶
197196ineq2i 4037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 / 𝑥𝐵𝑧 / 𝑥𝐶) = (𝑧 / 𝑥𝐵𝐶)
198193, 197eqtri 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑥(𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
199198eleq2i 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝑧 / 𝑥(𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
200192, 199bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
202189, 191, 2013bitrd 297 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)))
203202anbi2d 624 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) ↔ (𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
204 equequ2 2132 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑥 = 𝑤𝑥 = 𝑧))
205203, 204imbi12d 336 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)))
206205cbvralv 3382 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
207206ralbii 3188 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧))
208 nfv 2015 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧)
20968, 44nfin 4044 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥(𝑧 / 𝑥𝐵𝐶)
21042, 209nfel 2981 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)
211180, 210nfan 2004 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥(𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
212 nfv 2015 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 𝑤 = 𝑧
213211, 212nfim 2001 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
21466, 213nfral 3153 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)
215181anbi1d 625 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))))
216 equequ1 2131 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (𝑥 = 𝑧𝑤 = 𝑧))
217215, 216imbi12d 336 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
218217ralbidv 3194 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑤 → (∀𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
219208, 214, 218cbvral 3378 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝐴𝑧𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
220 biid 253 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
221 sbsbc 3665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
222 sbcel2 4212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ 𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶))
223 csbin 4234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶)
224 csbco 3766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝑤 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
225 csbconstg 3769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ V → 𝑧 / 𝑤𝐶 = 𝐶)
226194, 225ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑧 / 𝑤𝐶 = 𝐶
227224, 226ineq12i 4038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑤𝑤 / 𝑥𝐵𝑧 / 𝑤𝐶) = (𝑧 / 𝑥𝐵𝐶)
228 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
229223, 227, 2283eqtri 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) = (𝑧 / 𝑥𝐵𝐶)
230229eleq2i 2897 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝑧 / 𝑤(𝑤 / 𝑥𝐵𝐶) ↔ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶))
231221, 222, 2303bitrri 290 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑧 / 𝑥𝐵𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
232231anbi2i 618 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) ↔ (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)))
233232imbi1i 341 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
234233ralbii 3188 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
235234ralbii 3188 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
236220, 235bitri 267 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ 𝑦 ∈ (𝑧 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
237207, 219, 2363bitri 289 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝐴𝑤𝐴 ((𝑦 ∈ (𝐵𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
238112, 237sylib 210 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
239188, 178, 238syl2anc 581 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧))
240187, 239jca 509 . . . . . . . . . . . . . . . 16 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
241 reu2 3618 . . . . . . . . . . . . . . . 16 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ↔ (∃𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ ∀𝑤𝐴𝑧𝐴 ((𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = 𝑧)))
242240, 241sylibr 226 . . . . . . . . . . . . . . 15 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶))
243 riota1 6883 . . . . . . . . . . . . . . 15 (∃!𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
244242, 243syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → ((𝑤𝐴𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) ↔ (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤))
245185, 244mpbid 224 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑤𝐴 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) = 𝑤)
246183, 245eqtr2d 2861 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
247178, 246jca 509 . . . . . . . . . . 11 (((𝜑𝑤𝐴) ∧ 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶)) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
248247ex 403 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
249148, 150, 248syl2anc 581 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
250147, 249eximd 2261 . . . . . . . 8 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (𝑤 / 𝑥𝐵𝐶) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))))
251146, 250mpd 15 . . . . . . 7 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
252 df-rex 3122 . . . . . . 7 (∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ↔ ∃𝑦(𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ∧ 𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
253251, 252sylibr 226 . . . . . 6 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}) → ∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
254253ralrimiva 3174 . . . . 5 (𝜑 → ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
255136, 254jca 509 . . . 4 (𝜑 → (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
256 eqid 2824 . . . . 5 (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))) = (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶)))
257256fompt 40186 . . . 4 ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ↔ (∀𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)(𝑥𝐴 𝑦 ∈ (𝐵𝐶)) ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅}∃𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶)𝑤 = (𝑥𝐴 𝑦 ∈ (𝐵𝐶))))
258255, 257sylibr 226 . . 3 (𝜑 → (𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅})
259 fodomg 9659 . . 3 (( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ ( ran (𝑥𝐴𝐵) ∩ 𝐶) ↦ (𝑥𝐴 𝑦 ∈ (𝐵𝐶))):( ran (𝑥𝐴𝐵) ∩ 𝐶)–onto→{𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)))
26011, 258, 259sylc 65 . 2 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶))
261 domfi 8449 . 2 ((( ran (𝑥𝐴𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ≼ ( ran (𝑥𝐴𝐵) ∩ 𝐶)) → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
2627, 260, 261syl2anc 581 1 (𝜑 → {𝑥𝐴 ∣ (𝐵𝐶) ≠ ∅} ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880  w3a 1113   = wceq 1658  wex 1880  [wsb 2069  wcel 2166  wne 2998  wral 3116  wrex 3117  ∃!wreu 3118  {crab 3120  Vcvv 3413  [wsbc 3661  csb 3756  cin 3796  wss 3797  c0 4143   cuni 4657  Disj wdisj 4840   class class class wbr 4872  cmpt 4951  ran crn 5342  ontowfo 6120  crio 6864  cdom 8219  Fincfn 8221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-ac2 9599
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-disj 4841  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-se 5301  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-isom 6131  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-er 8008  df-map 8123  df-en 8222  df-dom 8223  df-fin 8225  df-card 9077  df-acn 9080  df-ac 9251
This theorem is referenced by:  fsumiunss  40601  sge0iunmptlemre  41422
  Copyright terms: Public domain W3C validator