MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptbasin Structured version   Visualization version   GIF version

Theorem ptbasin 22161
Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypothesis
Ref Expression
ptbas.1 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
Assertion
Ref Expression
ptbasin (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑋𝐵𝑌𝐵)) → (𝑋𝑌) ∈ 𝐵)
Distinct variable groups:   𝑥,𝑔,𝑦,𝑧,𝐴   𝑔,𝑌,𝑥   𝑔,𝐹,𝑥,𝑦,𝑧   𝑔,𝑋,𝑥,𝑧   𝑔,𝑉,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑔)   𝑋(𝑦)   𝑌(𝑦,𝑧)

Proof of Theorem ptbasin
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptbas.1 . . . . . 6 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
21elpt 22156 . . . . 5 (𝑋𝐵 ↔ ∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)))
31elpt 22156 . . . . 5 (𝑌𝐵 ↔ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦)))
42, 3anbi12i 628 . . . 4 ((𝑋𝐵𝑌𝐵) ↔ (∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))))
5 exdistrv 1956 . . . 4 (∃𝑎𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))) ↔ (∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))))
64, 5bitr4i 280 . . 3 ((𝑋𝐵𝑌𝐵) ↔ ∃𝑎𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))))
7 an4 654 . . . . 5 ((((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))) ↔ (((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))) ∧ (𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))))
8 an6 1441 . . . . . . . . 9 (((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))) ↔ ((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦)) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))))
9 df-3an 1085 . . . . . . . . 9 (((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦)) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))) ↔ (((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))))
108, 9bitri 277 . . . . . . . 8 (((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))) ↔ (((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))))
11 reeanv 3354 . . . . . . . . . . 11 (∃𝑐 ∈ Fin ∃𝑑 ∈ Fin (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ↔ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))
12 fveq2 6646 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑘 → (𝑎𝑦) = (𝑎𝑘))
13 fveq2 6646 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑘 → (𝑏𝑦) = (𝑏𝑘))
1412, 13ineq12d 4168 . . . . . . . . . . . . . . 15 (𝑦 = 𝑘 → ((𝑎𝑦) ∩ (𝑏𝑦)) = ((𝑎𝑘) ∩ (𝑏𝑘)))
1514cbvixpv 8457 . . . . . . . . . . . . . 14 X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) = X𝑘𝐴 ((𝑎𝑘) ∩ (𝑏𝑘))
16 simpl1l 1220 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → 𝐴𝑉)
17 unfi 8763 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) → (𝑐𝑑) ∈ Fin)
1817ad2antrl 726 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → (𝑐𝑑) ∈ Fin)
19 simpl1r 1221 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → 𝐹:𝐴⟶Top)
2019ffvelrnda 6827 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘𝐴) → (𝐹𝑘) ∈ Top)
21 simpl3l 1224 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦))
22 fveq2 6646 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑘 → (𝐹𝑦) = (𝐹𝑘))
2312, 22eleq12d 2905 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑘 → ((𝑎𝑦) ∈ (𝐹𝑦) ↔ (𝑎𝑘) ∈ (𝐹𝑘)))
2423rspccva 3601 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ 𝑘𝐴) → (𝑎𝑘) ∈ (𝐹𝑘))
2521, 24sylan 582 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘𝐴) → (𝑎𝑘) ∈ (𝐹𝑘))
26 simpl3r 1225 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))
2713, 22eleq12d 2905 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑘 → ((𝑏𝑦) ∈ (𝐹𝑦) ↔ (𝑏𝑘) ∈ (𝐹𝑘)))
2827rspccva 3601 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ 𝑘𝐴) → (𝑏𝑘) ∈ (𝐹𝑘))
2926, 28sylan 582 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘𝐴) → (𝑏𝑘) ∈ (𝐹𝑘))
30 inopn 21483 . . . . . . . . . . . . . . . 16 (((𝐹𝑘) ∈ Top ∧ (𝑎𝑘) ∈ (𝐹𝑘) ∧ (𝑏𝑘) ∈ (𝐹𝑘)) → ((𝑎𝑘) ∩ (𝑏𝑘)) ∈ (𝐹𝑘))
3120, 25, 29, 30syl3anc 1367 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘𝐴) → ((𝑎𝑘) ∩ (𝑏𝑘)) ∈ (𝐹𝑘))
32 simprrl 779 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦))
33 ssun1 4127 . . . . . . . . . . . . . . . . . . . 20 𝑐 ⊆ (𝑐𝑑)
34 sscon 4094 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ⊆ (𝑐𝑑) → (𝐴 ∖ (𝑐𝑑)) ⊆ (𝐴𝑐))
3533, 34ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∖ (𝑐𝑑)) ⊆ (𝐴𝑐)
3635sseli 3942 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝐴 ∖ (𝑐𝑑)) → 𝑘 ∈ (𝐴𝑐))
3722unieqd 4828 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑘 (𝐹𝑦) = (𝐹𝑘))
3812, 37eqeq12d 2836 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑘 → ((𝑎𝑦) = (𝐹𝑦) ↔ (𝑎𝑘) = (𝐹𝑘)))
3938rspccva 3601 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ 𝑘 ∈ (𝐴𝑐)) → (𝑎𝑘) = (𝐹𝑘))
4032, 36, 39syl2an 597 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐𝑑))) → (𝑎𝑘) = (𝐹𝑘))
41 simprrr 780 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))
42 ssun2 4128 . . . . . . . . . . . . . . . . . . . 20 𝑑 ⊆ (𝑐𝑑)
43 sscon 4094 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ⊆ (𝑐𝑑) → (𝐴 ∖ (𝑐𝑑)) ⊆ (𝐴𝑑))
4442, 43ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∖ (𝑐𝑑)) ⊆ (𝐴𝑑)
4544sseli 3942 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝐴 ∖ (𝑐𝑑)) → 𝑘 ∈ (𝐴𝑑))
4613, 37eqeq12d 2836 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑘 → ((𝑏𝑦) = (𝐹𝑦) ↔ (𝑏𝑘) = (𝐹𝑘)))
4746rspccva 3601 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦) ∧ 𝑘 ∈ (𝐴𝑑)) → (𝑏𝑘) = (𝐹𝑘))
4841, 45, 47syl2an 597 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐𝑑))) → (𝑏𝑘) = (𝐹𝑘))
4940, 48ineq12d 4168 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐𝑑))) → ((𝑎𝑘) ∩ (𝑏𝑘)) = ( (𝐹𝑘) ∩ (𝐹𝑘)))
50 inidm 4173 . . . . . . . . . . . . . . . 16 ( (𝐹𝑘) ∩ (𝐹𝑘)) = (𝐹𝑘)
5149, 50syl6eq 2871 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐𝑑))) → ((𝑎𝑘) ∩ (𝑏𝑘)) = (𝐹𝑘))
521, 16, 18, 31, 51elptr2 22158 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → X𝑘𝐴 ((𝑎𝑘) ∩ (𝑏𝑘)) ∈ 𝐵)
5315, 52eqeltrid 2915 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵)
5453expr 459 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ (𝑐 ∈ Fin ∧ 𝑑 ∈ Fin)) → ((∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵))
5554rexlimdvva 3281 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) → (∃𝑐 ∈ Fin ∃𝑑 ∈ Fin (∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵))
5611, 55syl5bir 245 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) → ((∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵))
57563expb 1116 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦)))) → ((∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵))
5857impr 457 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (((𝑎 Fn 𝐴𝑏 Fn 𝐴) ∧ (∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵)
5910, 58sylan2b 595 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵)
60 ineq12 4162 . . . . . . . . 9 ((𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦)) → (𝑋𝑌) = (X𝑦𝐴 (𝑎𝑦) ∩ X𝑦𝐴 (𝑏𝑦)))
61 ixpin 8465 . . . . . . . . 9 X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) = (X𝑦𝐴 (𝑎𝑦) ∩ X𝑦𝐴 (𝑏𝑦))
6260, 61syl6eqr 2873 . . . . . . . 8 ((𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦)) → (𝑋𝑌) = X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)))
6362eleq1d 2895 . . . . . . 7 ((𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦)) → ((𝑋𝑌) ∈ 𝐵X𝑦𝐴 ((𝑎𝑦) ∩ (𝑏𝑦)) ∈ 𝐵))
6459, 63syl5ibrcom 249 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)))) → ((𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦)) → (𝑋𝑌) ∈ 𝐵))
6564expimpd 456 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦))) ∧ (𝑋 = X𝑦𝐴 (𝑎𝑦) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))) → (𝑋𝑌) ∈ 𝐵))
667, 65syl5bi 244 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ((((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))) → (𝑋𝑌) ∈ 𝐵))
6766exlimdvv 1935 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃𝑎𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑎𝑦) ∈ (𝐹𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴𝑐)(𝑎𝑦) = (𝐹𝑦)) ∧ 𝑋 = X𝑦𝐴 (𝑎𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑏𝑦) ∈ (𝐹𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴𝑑)(𝑏𝑦) = (𝐹𝑦)) ∧ 𝑌 = X𝑦𝐴 (𝑏𝑦))) → (𝑋𝑌) ∈ 𝐵))
686, 67syl5bi 244 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → ((𝑋𝐵𝑌𝐵) → (𝑋𝑌) ∈ 𝐵))
6968imp 409 1 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑋𝐵𝑌𝐵)) → (𝑋𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083   = wceq 1537  wex 1780  wcel 2114  {cab 2798  wral 3125  wrex 3126  cdif 3910  cun 3911  cin 3912  wss 3913   cuni 4814   Fn wfn 6326  wf 6327  cfv 6331  Xcixp 8439  Fincfn 8487  Topctop 21477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-oadd 8084  df-er 8267  df-ixp 8440  df-en 8488  df-fin 8491  df-top 21478
This theorem is referenced by:  ptbasin2  22162
  Copyright terms: Public domain W3C validator