| 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
|
syl5bi |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 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
|
ffvelrnd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 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 ∧ 𝐼 ∈ 𝐴 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑌 ↦ ( 𝑥 ‘ 𝐼 ) ) “ 𝑈 ) ∈ ( 𝐹 ‘ 𝐼 ) ) |