This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 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 biimtrrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 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 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) )
67 66 exlimdvv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∃ 𝑎 ∃ 𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) )
68 6 67 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) )
69 68 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 )