Step | Hyp | Ref
| Expression |
1 | | simp-6l 806 |
. . . . . . . 8
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋)) |
2 | | simp-7l 808 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋)) |
3 | | simp-4r 803 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈) |
4 | | simplr 788 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈) |
5 | | ustincl 21821 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑢 ∈ 𝑈) → (𝑤 ∩ 𝑢) ∈ 𝑈) |
6 | 2, 3, 4, 5 | syl3anc 1318 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑤 ∩ 𝑢) ∈ 𝑈) |
7 | | simpllr 795 |
. . . . . . . . . 10
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → 𝑎 = (𝑤 “ {𝑝})) |
8 | | ineq12 3771 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑤 “ {𝑝}) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑎 ∩ 𝑏) = ((𝑤 “ {𝑝}) ∩ (𝑢 “ {𝑝}))) |
9 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑝 ∈ V |
10 | | inimasn 5469 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ V → ((𝑤 ∩ 𝑢) “ {𝑝}) = ((𝑤 “ {𝑝}) ∩ (𝑢 “ {𝑝}))) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑤 ∩ 𝑢) “ {𝑝}) = ((𝑤 “ {𝑝}) ∩ (𝑢 “ {𝑝})) |
12 | 8, 11 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑤 “ {𝑝}) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑎 ∩ 𝑏) = ((𝑤 ∩ 𝑢) “ {𝑝})) |
13 | 7, 12 | sylancom 698 |
. . . . . . . . 9
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑎 ∩ 𝑏) = ((𝑤 ∩ 𝑢) “ {𝑝})) |
14 | | imaeq1 5380 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑤 ∩ 𝑢) → (𝑥 “ {𝑝}) = ((𝑤 ∩ 𝑢) “ {𝑝})) |
15 | 14 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑤 ∩ 𝑢) → ((𝑎 ∩ 𝑏) = (𝑥 “ {𝑝}) ↔ (𝑎 ∩ 𝑏) = ((𝑤 ∩ 𝑢) “ {𝑝}))) |
16 | 15 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑤 ∩ 𝑢) ∈ 𝑈 ∧ (𝑎 ∩ 𝑏) = ((𝑤 ∩ 𝑢) “ {𝑝})) → ∃𝑥 ∈ 𝑈 (𝑎 ∩ 𝑏) = (𝑥 “ {𝑝})) |
17 | 6, 13, 16 | syl2anc 691 |
. . . . . . . 8
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → ∃𝑥 ∈ 𝑈 (𝑎 ∩ 𝑏) = (𝑥 “ {𝑝})) |
18 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
19 | 18 | inex1 4727 |
. . . . . . . . . 10
⊢ (𝑎 ∩ 𝑏) ∈ V |
20 | | utopustuq.1 |
. . . . . . . . . . 11
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
21 | 20 | ustuqtoplem 21853 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑎 ∩ 𝑏) ∈ V) → ((𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝) ↔ ∃𝑥 ∈ 𝑈 (𝑎 ∩ 𝑏) = (𝑥 “ {𝑝}))) |
22 | 19, 21 | mpan2 703 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝) ↔ ∃𝑥 ∈ 𝑈 (𝑎 ∩ 𝑏) = (𝑥 “ {𝑝}))) |
23 | 22 | biimpar 501 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ ∃𝑥 ∈ 𝑈 (𝑎 ∩ 𝑏) = (𝑥 “ {𝑝})) → (𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
24 | 1, 17, 23 | syl2anc 691 |
. . . . . . 7
⊢
((((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) ∧ 𝑢 ∈ 𝑈) ∧ 𝑏 = (𝑢 “ {𝑝})) → (𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
25 | | simp-4l 802 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋)) |
26 | | simpllr 795 |
. . . . . . . 8
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑏 ∈ (𝑁‘𝑝)) |
27 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
28 | 20 | ustuqtoplem 21853 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ∈ V) → (𝑏 ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 𝑏 = (𝑢 “ {𝑝}))) |
29 | 27, 28 | mpan2 703 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑏 ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 𝑏 = (𝑢 “ {𝑝}))) |
30 | 29 | biimpa 500 |
. . . . . . . 8
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → ∃𝑢 ∈ 𝑈 𝑏 = (𝑢 “ {𝑝})) |
31 | 25, 26, 30 | syl2anc 691 |
. . . . . . 7
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 𝑏 = (𝑢 “ {𝑝})) |
32 | 24, 31 | r19.29a 3060 |
. . . . . 6
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
33 | 20 | ustuqtoplem 21853 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
34 | 18, 33 | mpan2 703 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))) |
35 | 34 | biimpa 500 |
. . . . . . 7
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})) |
37 | 32, 36 | r19.29a 3060 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑏 ∈ (𝑁‘𝑝)) → (𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
38 | 37 | ralrimiva 2949 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∀𝑏 ∈ (𝑁‘𝑝)(𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
39 | 38 | ralrimiva 2949 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ∀𝑎 ∈ (𝑁‘𝑝)∀𝑏 ∈ (𝑁‘𝑝)(𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝)) |
40 | | fvex 6113 |
. . . 4
⊢ (𝑁‘𝑝) ∈ V |
41 | | inficl 8214 |
. . . 4
⊢ ((𝑁‘𝑝) ∈ V → (∀𝑎 ∈ (𝑁‘𝑝)∀𝑏 ∈ (𝑁‘𝑝)(𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝) ↔ (fi‘(𝑁‘𝑝)) = (𝑁‘𝑝))) |
42 | 40, 41 | ax-mp 5 |
. . 3
⊢
(∀𝑎 ∈
(𝑁‘𝑝)∀𝑏 ∈ (𝑁‘𝑝)(𝑎 ∩ 𝑏) ∈ (𝑁‘𝑝) ↔ (fi‘(𝑁‘𝑝)) = (𝑁‘𝑝)) |
43 | 39, 42 | sylib 207 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) = (𝑁‘𝑝)) |
44 | | eqimss 3620 |
. 2
⊢
((fi‘(𝑁‘𝑝)) = (𝑁‘𝑝) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
45 | 43, 44 | syl 17 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |