Step | Hyp | Ref
| Expression |
1 | | fnresi 5922 |
. . . . . . 7
⊢ ( I
↾ 𝑋) Fn 𝑋 |
2 | | fnsnfv 6168 |
. . . . . . 7
⊢ ((( I
↾ 𝑋) Fn 𝑋 ∧ 𝑝 ∈ 𝑋) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
3 | 1, 2 | mpan 702 |
. . . . . 6
⊢ (𝑝 ∈ 𝑋 → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
4 | 3 | ad4antlr 765 |
. . . . 5
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝})) |
5 | | simp-4l 802 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋)) |
6 | | simplr 788 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑤 ∈ 𝑈) |
7 | | ustdiag 21822 |
. . . . . . 7
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑤) |
8 | 5, 6, 7 | syl2anc 691 |
. . . . . 6
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ( I ↾ 𝑋) ⊆ 𝑤) |
9 | | imass1 5419 |
. . . . . 6
⊢ (( I
↾ 𝑋) ⊆ 𝑤 → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝})) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝})) |
11 | 4, 10 | eqsstrd 3602 |
. . . 4
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝})) |
12 | | fvex 6113 |
. . . . 5
⊢ (( I
↾ 𝑋)‘𝑝) ∈ V |
13 | 12 | snss 4259 |
. . . 4
⊢ ((( I
↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝}) ↔ {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝})) |
14 | 11, 13 | sylibr 223 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝})) |
15 | | fvresi 6344 |
. . . . 5
⊢ (𝑝 ∈ 𝑋 → (( I ↾ 𝑋)‘𝑝) = 𝑝) |
16 | 15 | eqcomd 2616 |
. . . 4
⊢ (𝑝 ∈ 𝑋 → 𝑝 = (( I ↾ 𝑋)‘𝑝)) |
17 | 16 | ad4antlr 765 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 = (( I ↾ 𝑋)‘𝑝)) |
18 | | simpr 476 |
. . 3
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑎 = (𝑤 “ {𝑝})) |
19 | 14, 17, 18 | 3eltr4d 2703 |
. 2
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 ∈ 𝑎) |
20 | | vex 3176 |
. . . 4
⊢ 𝑎 ∈ V |
21 | | utopustuq.1 |
. . . . 5
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
22 | 21 | ustuqtoplem 21853 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
23 | 20, 22 | mpan2 703 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
24 | 23 | biimpa 500 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})) |
25 | 19, 24 | r19.29a 3060 |
1
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |