Metamath Proof Explorer


Theorem ptbasin

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.1 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
Assertion ptbasin ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ptbas.1 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
2 1 elpt ( 𝑋𝐵 ↔ ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) )
3 1 elpt ( 𝑌𝐵 ↔ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) )
4 2 3 anbi12i ( ( 𝑋𝐵𝑌𝐵 ) ↔ ( ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) )
5 exdistrv ( ∃ 𝑎𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) ↔ ( ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) )
6 4 5 bitr4i ( ( 𝑋𝐵𝑌𝐵 ) ↔ ∃ 𝑎𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) )
7 an4 ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ∧ ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) )
8 an6 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ↔ ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) )
9 df-3an ( ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) )
10 8 9 bitri ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) )
11 reeanv ( ∃ 𝑐 ∈ Fin ∃ 𝑑 ∈ Fin ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ↔ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) )
12 fveq2 ( 𝑦 = 𝑘 → ( 𝑎𝑦 ) = ( 𝑎𝑘 ) )
13 fveq2 ( 𝑦 = 𝑘 → ( 𝑏𝑦 ) = ( 𝑏𝑘 ) )
14 12 13 ineq12d ( 𝑦 = 𝑘 → ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) = ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) )
15 14 cbvixpv X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) = X 𝑘𝐴 ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) )
16 simpl1l ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → 𝐴𝑉 )
17 unfi ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) → ( 𝑐𝑑 ) ∈ Fin )
18 17 ad2antrl ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ( 𝑐𝑑 ) ∈ Fin )
19 simpl1r ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → 𝐹 : 𝐴 ⟶ Top )
20 19 ffvelrnda ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘𝐴 ) → ( 𝐹𝑘 ) ∈ Top )
21 simpl3l ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) )
22 fveq2 ( 𝑦 = 𝑘 → ( 𝐹𝑦 ) = ( 𝐹𝑘 ) )
23 12 22 eleq12d ( 𝑦 = 𝑘 → ( ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ↔ ( 𝑎𝑘 ) ∈ ( 𝐹𝑘 ) ) )
24 23 rspccva ( ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ 𝑘𝐴 ) → ( 𝑎𝑘 ) ∈ ( 𝐹𝑘 ) )
25 21 24 sylan ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘𝐴 ) → ( 𝑎𝑘 ) ∈ ( 𝐹𝑘 ) )
26 simpl3r ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) )
27 13 22 eleq12d ( 𝑦 = 𝑘 → ( ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ↔ ( 𝑏𝑘 ) ∈ ( 𝐹𝑘 ) ) )
28 27 rspccva ( ( ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ 𝑘𝐴 ) → ( 𝑏𝑘 ) ∈ ( 𝐹𝑘 ) )
29 26 28 sylan ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘𝐴 ) → ( 𝑏𝑘 ) ∈ ( 𝐹𝑘 ) )
30 inopn ( ( ( 𝐹𝑘 ) ∈ Top ∧ ( 𝑎𝑘 ) ∈ ( 𝐹𝑘 ) ∧ ( 𝑏𝑘 ) ∈ ( 𝐹𝑘 ) ) → ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) ∈ ( 𝐹𝑘 ) )
31 20 25 29 30 syl3anc ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘𝐴 ) → ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) ∈ ( 𝐹𝑘 ) )
32 simprrl ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) )
33 ssun1 𝑐 ⊆ ( 𝑐𝑑 )
34 sscon ( 𝑐 ⊆ ( 𝑐𝑑 ) → ( 𝐴 ∖ ( 𝑐𝑑 ) ) ⊆ ( 𝐴𝑐 ) )
35 33 34 ax-mp ( 𝐴 ∖ ( 𝑐𝑑 ) ) ⊆ ( 𝐴𝑐 )
36 35 sseli ( 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) → 𝑘 ∈ ( 𝐴𝑐 ) )
37 22 unieqd ( 𝑦 = 𝑘 ( 𝐹𝑦 ) = ( 𝐹𝑘 ) )
38 12 37 eqeq12d ( 𝑦 = 𝑘 → ( ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ↔ ( 𝑎𝑘 ) = ( 𝐹𝑘 ) ) )
39 38 rspccva ( ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ 𝑘 ∈ ( 𝐴𝑐 ) ) → ( 𝑎𝑘 ) = ( 𝐹𝑘 ) )
40 32 36 39 syl2an ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) ) → ( 𝑎𝑘 ) = ( 𝐹𝑘 ) )
41 simprrr ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) )
42 ssun2 𝑑 ⊆ ( 𝑐𝑑 )
43 sscon ( 𝑑 ⊆ ( 𝑐𝑑 ) → ( 𝐴 ∖ ( 𝑐𝑑 ) ) ⊆ ( 𝐴𝑑 ) )
44 42 43 ax-mp ( 𝐴 ∖ ( 𝑐𝑑 ) ) ⊆ ( 𝐴𝑑 )
45 44 sseli ( 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) → 𝑘 ∈ ( 𝐴𝑑 ) )
46 13 37 eqeq12d ( 𝑦 = 𝑘 → ( ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ↔ ( 𝑏𝑘 ) = ( 𝐹𝑘 ) ) )
47 46 rspccva ( ( ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ∧ 𝑘 ∈ ( 𝐴𝑑 ) ) → ( 𝑏𝑘 ) = ( 𝐹𝑘 ) )
48 41 45 47 syl2an ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) ) → ( 𝑏𝑘 ) = ( 𝐹𝑘 ) )
49 40 48 ineq12d ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) ) → ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) = ( ( 𝐹𝑘 ) ∩ ( 𝐹𝑘 ) ) )
50 inidm ( ( 𝐹𝑘 ) ∩ ( 𝐹𝑘 ) ) = ( 𝐹𝑘 )
51 49 50 eqtrdi ( ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐𝑑 ) ) ) → ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) = ( 𝐹𝑘 ) )
52 1 16 18 31 51 elptr2 ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → X 𝑘𝐴 ( ( 𝑎𝑘 ) ∩ ( 𝑏𝑘 ) ) ∈ 𝐵 )
53 15 52 eqeltrid ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 )
54 53 expr ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 ) )
55 54 rexlimdvva ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) → ( ∃ 𝑐 ∈ Fin ∃ 𝑑 ∈ Fin ( ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 ) )
56 11 55 syl5bir ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) → ( ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 ) )
57 56 3expb ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ) → ( ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 ) )
58 57 impr ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( ( ( 𝑎 Fn 𝐴𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 )
59 10 58 sylan2b ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 )
60 ineq12 ( ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) → ( 𝑋𝑌 ) = ( X 𝑦𝐴 ( 𝑎𝑦 ) ∩ X 𝑦𝐴 ( 𝑏𝑦 ) ) )
61 ixpin X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) = ( X 𝑦𝐴 ( 𝑎𝑦 ) ∩ X 𝑦𝐴 ( 𝑏𝑦 ) )
62 60 61 eqtr4di ( ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) → ( 𝑋𝑌 ) = X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) )
63 62 eleq1d ( ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) → ( ( 𝑋𝑌 ) ∈ 𝐵X 𝑦𝐴 ( ( 𝑎𝑦 ) ∩ ( 𝑏𝑦 ) ) ∈ 𝐵 ) )
64 59 63 syl5ibrcom ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ) → ( ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) → ( 𝑋𝑌 ) ∈ 𝐵 ) )
65 64 expimpd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ) ∧ ( 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) → ( 𝑋𝑌 ) ∈ 𝐵 ) )
66 7 65 syl5bi ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) → ( 𝑋𝑌 ) ∈ 𝐵 ) )
67 66 exlimdvv ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ∃ 𝑎𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑎𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑐 ) ( 𝑎𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑋 = X 𝑦𝐴 ( 𝑎𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑏𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑑 ) ( 𝑏𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑌 = X 𝑦𝐴 ( 𝑏𝑦 ) ) ) → ( 𝑋𝑌 ) ∈ 𝐵 ) )
68 6 67 syl5bi ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋𝑌 ) ∈ 𝐵 ) )
69 68 imp ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋𝑌 ) ∈ 𝐵 )