Step |
Hyp |
Ref |
Expression |
1 |
|
utopustuq.1 |
⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) |
2 |
|
simp-6l |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ) |
3 |
|
simp-7l |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
4 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑤 ∈ 𝑈 ) |
5 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → 𝑢 ∈ 𝑈 ) |
6 |
|
ustincl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 ) |
7 |
3 4 5 6
|
syl3anc |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 ) |
8 |
|
ineq12 |
⊢ ( ( 𝑎 = ( 𝑤 “ { 𝑝 } ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) ) ) |
9 |
|
inimasn |
⊢ ( 𝑝 ∈ V → ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) ) ) |
10 |
9
|
elv |
⊢ ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) = ( ( 𝑤 “ { 𝑝 } ) ∩ ( 𝑢 “ { 𝑝 } ) ) |
11 |
8 10
|
eqtr4di |
⊢ ( ( 𝑎 = ( 𝑤 “ { 𝑝 } ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) ) |
12 |
11
|
ad4ant24 |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) ) |
13 |
|
imaeq1 |
⊢ ( 𝑥 = ( 𝑤 ∩ 𝑢 ) → ( 𝑥 “ { 𝑝 } ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) ) |
14 |
13
|
rspceeqv |
⊢ ( ( ( 𝑤 ∩ 𝑢 ) ∈ 𝑈 ∧ ( 𝑎 ∩ 𝑏 ) = ( ( 𝑤 ∩ 𝑢 ) “ { 𝑝 } ) ) → ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) |
15 |
7 12 14
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) |
16 |
|
vex |
⊢ 𝑎 ∈ V |
17 |
16
|
inex1 |
⊢ ( 𝑎 ∩ 𝑏 ) ∈ V |
18 |
1
|
ustuqtoplem |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ ( 𝑎 ∩ 𝑏 ) ∈ V ) → ( ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) ) |
19 |
17 18
|
mpan2 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) ) |
20 |
19
|
biimpar |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑈 ( 𝑎 ∩ 𝑏 ) = ( 𝑥 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
21 |
2 15 20
|
syl2anc |
⊢ ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑏 = ( 𝑢 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
22 |
1
|
ustuqtoplem |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑏 ∈ V ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) ) |
23 |
22
|
elvd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) ) |
24 |
23
|
biimpa |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) |
25 |
24
|
ad5ant13 |
⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑢 ∈ 𝑈 𝑏 = ( 𝑢 “ { 𝑝 } ) ) |
26 |
21 25
|
r19.29a |
⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
27 |
1
|
ustuqtoplem |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ V ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) |
28 |
27
|
elvd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) ) |
29 |
28
|
biimpa |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) |
30 |
29
|
adantr |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) |
31 |
26 30
|
r19.29a |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
32 |
31
|
ralrimiva |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
33 |
32
|
ralrimiva |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ) |
34 |
|
fvex |
⊢ ( 𝑁 ‘ 𝑝 ) ∈ V |
35 |
|
inficl |
⊢ ( ( 𝑁 ‘ 𝑝 ) ∈ V → ( ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) ) ) |
36 |
34 35
|
ax-mp |
⊢ ( ∀ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ( 𝑎 ∩ 𝑏 ) ∈ ( 𝑁 ‘ 𝑝 ) ↔ ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) ) |
37 |
33 36
|
sylib |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) ) |
38 |
|
eqimss |
⊢ ( ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑁 ‘ 𝑝 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) ) |
39 |
37 38
|
syl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) ) |