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

Metamath Proof Explorer

Theorem ptpjopn

Description: The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses ptpjcn.1 ⊢ 𝑌 = ∪ 𝐽
ptpjcn.2 ⊢ 𝐽 = ( ∏t ‘ 𝐹 )
Assertion ptpjopn ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) “ 𝑈 ) ∈ ( 𝐹 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 ptpjcn.1 ⊢ 𝑌 = ∪ 𝐽
2 ptpjcn.2 ⊢ 𝐽 = ( ∏t ‘ 𝐹 )
3 df-ima ⊢ ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) “ 𝑈 ) = ran ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) ↾ 𝑈 )
4 elssuni ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
5 4 1 sseqtrrdi ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ 𝑌 )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ 𝑌 )
7 6 resmptd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) ↾ 𝑈 ) = ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) )
8 7 rneqd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ran ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) ↾ 𝑈 ) = ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) )
9 3 8 eqtrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) “ 𝑈 ) = ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) )
10 ffn ⊢ ( 𝐹 : 𝐴 ⟶ Top → 𝐹 Fn 𝐴 )
11 eqid ⊢ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
12 11 ptval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
13 10 12 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
14 2 13 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → 𝐽 = ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
15 14 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) → 𝐽 = ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
16 15 eleq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) → ( 𝑈 ∈ 𝐽 ↔ 𝑈 ∈ ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) ) )
17 16 biimpa ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ∈ ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
18 tg2 ⊢ ( ( 𝑈 ∈ ( topGen ‘ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) ∧ 𝑠 ∈ 𝑈 ) → ∃ 𝑤 ∈ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) )
19 17 18 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ∃ 𝑤 ∈ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) )
20 vex ⊢ 𝑤 ∈ V
21 eqeq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
22 21 anbi2d ⊢ ( 𝑠 = 𝑤 → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
23 22 exbidv ⊢ ( 𝑠 = 𝑤 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) )
24 20 23 elab ⊢ ( 𝑤 ∈ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
25 fveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝐼 ) )
26 fveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐼 ) )
27 25 26 eleq12d ⊢ ( 𝑦 = 𝐼 → ( ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝐼 ) ∈ ( 𝐹 ‘ 𝐼 ) ) )
28 simplr2 ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) )
29 simpl3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → 𝐼 ∈ 𝐴 )
30 29 ad3antrrr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → 𝐼 ∈ 𝐴 )
31 27 28 30 rspcdva ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ( 𝑔 ‘ 𝐼 ) ∈ ( 𝐹 ‘ 𝐼 ) )
32 fveq2 ⊢ ( 𝑦 = 𝐼 → ( 𝑠 ‘ 𝑦 ) = ( 𝑠 ‘ 𝐼 ) )
33 32 25 eleq12d ⊢ ( 𝑦 = 𝐼 → ( ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑠 ‘ 𝐼 ) ∈ ( 𝑔 ‘ 𝐼 ) ) )
34 vex ⊢ 𝑠 ∈ V
35 34 elixp ⊢ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑠 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) ) )
36 35 simprbi ⊢ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) )
37 36 ad2antrl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) )
38 33 37 30 rspcdva ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ( 𝑠 ‘ 𝐼 ) ∈ ( 𝑔 ‘ 𝐼 ) )
39 simplrr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 )
40 simplrl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) ∧ 𝑛 = 𝐼 ) → 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) )
41 fveq2 ⊢ ( 𝑛 = 𝐼 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝐼 ) )
42 41 adantl ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) ∧ 𝑛 = 𝐼 ) → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝐼 ) )
43 40 42 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) ∧ 𝑛 = 𝐼 ) → 𝑘 ∈ ( 𝑔 ‘ 𝑛 ) )
44 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑠 ‘ 𝑦 ) = ( 𝑠 ‘ 𝑛 ) )
45 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑛 ) )
46 44 45 eleq12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑠 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
47 simplrl ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) → 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
48 47 36 syl ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑠 ‘ 𝑦 ) ∈ ( 𝑔 ‘ 𝑦 ) )
49 simprr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) → 𝑛 ∈ 𝐴 )
50 46 48 49 rspcdva ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) → ( 𝑠 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
51 50 adantr ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) ∧ ¬ 𝑛 = 𝐼 ) → ( 𝑠 ‘ 𝑛 ) ∈ ( 𝑔 ‘ 𝑛 ) )
52 43 51 ifclda ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ∧ 𝑛 ∈ 𝐴 ) ) → if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ∈ ( 𝑔 ‘ 𝑛 ) )
53 52 anassrs ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) ∧ 𝑛 ∈ 𝐴 ) → if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ∈ ( 𝑔 ‘ 𝑛 ) )
54 53 ralrimiva ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ∈ ( 𝑔 ‘ 𝑛 ) )
55 simpll1 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → 𝐴 ∈ 𝑉 )
56 55 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → 𝐴 ∈ 𝑉 )
57 mptelixpg ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ( 𝑔 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
58 56 57 syl ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ( 𝑔 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ∈ ( 𝑔 ‘ 𝑛 ) ) )
59 54 58 mpbird ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ( 𝑔 ‘ 𝑛 ) )
60 fveq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑦 ) )
61 60 cbvixpv ⊢ X 𝑛 ∈ 𝐴 ( 𝑔 ‘ 𝑛 ) = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 )
62 59 61 eleqtrdi ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
63 39 62 sseldd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ 𝑈 )
64 30 adantr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → 𝐼 ∈ 𝐴 )
65 iftrue ⊢ ( 𝑛 = 𝐼 → if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) = 𝑘 )
66 eqid ⊢ ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) )
67 vex ⊢ 𝑘 ∈ V
68 65 66 67 fvmpt ⊢ ( 𝐼 ∈ 𝐴 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ‘ 𝐼 ) = 𝑘 )
69 64 68 syl ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ‘ 𝐼 ) = 𝑘 )
70 69 eqcomd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → 𝑘 = ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ‘ 𝐼 ) )
71 fveq1 ⊢ ( 𝑥 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) → ( 𝑥 ‘ 𝐼 ) = ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ‘ 𝐼 ) )
72 71 rspceeqv ⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ∈ 𝑈 ∧ 𝑘 = ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝐼 , 𝑘 , ( 𝑠 ‘ 𝑛 ) ) ) ‘ 𝐼 ) ) → ∃ 𝑥 ∈ 𝑈 𝑘 = ( 𝑥 ‘ 𝐼 ) )
73 63 70 72 syl2anc ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → ∃ 𝑥 ∈ 𝑈 𝑘 = ( 𝑥 ‘ 𝐼 ) )
74 eqid ⊢ ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) = ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) )
75 74 elrnmpt ⊢ ( 𝑘 ∈ V → ( 𝑘 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ↔ ∃ 𝑥 ∈ 𝑈 𝑘 = ( 𝑥 ‘ 𝐼 ) ) )
76 75 elv ⊢ ( 𝑘 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ↔ ∃ 𝑥 ∈ 𝑈 𝑘 = ( 𝑥 ‘ 𝐼 ) )
77 73 76 sylibr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) ) → 𝑘 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) )
78 77 ex ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ( 𝑘 ∈ ( 𝑔 ‘ 𝐼 ) → 𝑘 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
79 78 ssrdv ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ( 𝑔 ‘ 𝐼 ) ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) )
80 eleq2 ⊢ ( 𝑧 = ( 𝑔 ‘ 𝐼 ) → ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ↔ ( 𝑠 ‘ 𝐼 ) ∈ ( 𝑔 ‘ 𝐼 ) ) )
81 sseq1 ⊢ ( 𝑧 = ( 𝑔 ‘ 𝐼 ) → ( 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ↔ ( 𝑔 ‘ 𝐼 ) ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
82 80 81 anbi12d ⊢ ( 𝑧 = ( 𝑔 ‘ 𝐼 ) → ( ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ↔ ( ( 𝑠 ‘ 𝐼 ) ∈ ( 𝑔 ‘ 𝐼 ) ∧ ( 𝑔 ‘ 𝐼 ) ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
83 82 rspcev ⊢ ( ( ( 𝑔 ‘ 𝐼 ) ∈ ( 𝐹 ‘ 𝐼 ) ∧ ( ( 𝑠 ‘ 𝐼 ) ∈ ( 𝑔 ‘ 𝐼 ) ∧ ( 𝑔 ‘ 𝐼 ) ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
84 31 38 79 83 syl12anc ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
85 84 ex ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
86 eleq2 ⊢ ( 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( 𝑠 ∈ 𝑤 ↔ 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
87 sseq1 ⊢ ( 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( 𝑤 ⊆ 𝑈 ↔ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) )
88 86 87 anbi12d ⊢ ( 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) ↔ ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) ) )
89 88 imbi1d ⊢ ( 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ↔ ( ( 𝑠 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ) )
90 85 89 syl5ibrcom ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ) )
91 90 expimpd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ) )
92 91 exlimdv ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑤 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ) )
93 24 92 biimtrid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ( 𝑤 ∈ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) ) )
94 93 rexlimdv ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ( ∃ 𝑤 ∈ { 𝑠 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑠 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( 𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
95 19 94 mpd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝑈 ) → ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
96 95 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑠 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
97 fvex ⊢ ( 𝑠 ‘ 𝐼 ) ∈ V
98 97 rgenw ⊢ ∀ 𝑠 ∈ 𝑈 ( 𝑠 ‘ 𝐼 ) ∈ V
99 fveq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 ‘ 𝐼 ) = ( 𝑠 ‘ 𝐼 ) )
100 99 cbvmptv ⊢ ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) = ( 𝑠 ∈ 𝑈 ↦ ( 𝑠 ‘ 𝐼 ) )
101 eleq1 ⊢ ( 𝑦 = ( 𝑠 ‘ 𝐼 ) → ( 𝑦 ∈ 𝑧 ↔ ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ) )
102 101 anbi1d ⊢ ( 𝑦 = ( 𝑠 ‘ 𝐼 ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ↔ ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
103 102 rexbidv ⊢ ( 𝑦 = ( 𝑠 ‘ 𝐼 ) → ( ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ↔ ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
104 100 103 ralrnmptw ⊢ ( ∀ 𝑠 ∈ 𝑈 ( 𝑠 ‘ 𝐼 ) ∈ V → ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ↔ ∀ 𝑠 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
105 98 104 ax-mp ⊢ ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ↔ ∀ 𝑠 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( ( 𝑠 ‘ 𝐼 ) ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
106 96 105 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) )
107 simpl2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → 𝐹 : 𝐴 ⟶ Top )
108 107 29 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 ‘ 𝐼 ) ∈ Top )
109 eltop2 ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ Top → ( ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∈ ( 𝐹 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
110 108 109 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∈ ( 𝐹 ‘ 𝐼 ) ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∃ 𝑧 ∈ ( 𝐹 ‘ 𝐼 ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ) ) )
111 106 110 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ran ( 𝑥 ∈ 𝑈 ↦ ( 𝑥 ‘ 𝐼 ) ) ∈ ( 𝐹 ‘ 𝐼 ) )
112 9 111 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) “ 𝑈 ) ∈ ( 𝐹 ‘ 𝐼 ) )