Step | Hyp | Ref
| Expression |
1 | | fnresi 6241 |
. . . . . . 7
⊢ ( I
↾ 𝑋) Fn 𝑋 |
2 | | fnsnfv 6505 |
. . . . . . 7
⊢ ((( I
↾ 𝑋) Fn 𝑋 ∧ 𝑝 ∈ 𝑋) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
3 | 1, 2 | mpan 681 |
. . . . . 6
⊢ (𝑝 ∈ 𝑋 → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
4 | 3 | ad4antlr 726 |
. . . . 5
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
5 | | simp-4l 801 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋)) |
6 | | simplr 785 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑤 ∈ 𝑈) |
7 | | ustdiag 22382 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑤) |
8 | 5, 6, 7 | syl2anc 579 |
. . . . . 6
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ( I ↾ 𝑋) ⊆ 𝑤) |
9 | | imass1 5741 |
. . . . . 6
⊢ (( I
↾ 𝑋) ⊆ 𝑤 → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝})) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝})) |
11 | 4, 10 | eqsstrd 3864 |
. . . 4
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝})) |
12 | | fvex 6446 |
. . . . 5
⊢ (( I
↾ 𝑋)‘𝑝) ∈ V |
13 | 12 | snss 4535 |
. . . 4
⊢ ((( I
↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝}) ↔ {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝})) |
14 | 11, 13 | sylibr 226 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝})) |
15 | | fvresi 6691 |
. . . . 5
⊢ (𝑝 ∈ 𝑋 → (( I ↾ 𝑋)‘𝑝) = 𝑝) |
16 | 15 | eqcomd 2831 |
. . . 4
⊢ (𝑝 ∈ 𝑋 → 𝑝 = (( I ↾ 𝑋)‘𝑝)) |
17 | 16 | ad4antlr 726 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 = (( I ↾ 𝑋)‘𝑝)) |
18 | | simpr 479 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑎 = (𝑤 “ {𝑝})) |
19 | 14, 17, 18 | 3eltr4d 2921 |
. 2
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 ∈ 𝑎) |
20 | | utopustuq.1 |
. . . . 5
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
21 | 20 | ustuqtoplem 22413 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
22 | 21 | elvd 3419 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
23 | 22 | biimpa 470 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})) |
24 | 19, 23 | r19.29a 3288 |
1
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |