Step |
Hyp |
Ref |
Expression |
1 |
|
ucnprima.1 |
⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
2 |
|
ucnprima.2 |
⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) |
3 |
|
ucnprima.3 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ) |
4 |
|
ucnprima.4 |
⊢ ( 𝜑 → 𝑊 ∈ 𝑉 ) |
5 |
|
ucnprima.5 |
⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ 〈 ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) 〉 ) |
6 |
1 2 3 4 5
|
ucnima |
⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) |
7 |
5
|
mpofun |
⊢ Fun 𝐺 |
8 |
|
ustssxp |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) ) |
9 |
1 8
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) ) |
10 |
|
opex |
⊢ 〈 ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) 〉 ∈ V |
11 |
5 10
|
dmmpo |
⊢ dom 𝐺 = ( 𝑋 × 𝑋 ) |
12 |
9 11
|
sseqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ dom 𝐺 ) |
13 |
|
funimass3 |
⊢ ( ( Fun 𝐺 ∧ 𝑟 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) ) |
14 |
7 12 13
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) ) |
15 |
14
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) ) |
16 |
6 15
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) |
17 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) |
18 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ∈ 𝑈 ) |
19 |
|
cnvimass |
⊢ ( ◡ 𝐺 “ 𝑊 ) ⊆ dom 𝐺 |
20 |
19 11
|
sseqtri |
⊢ ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 ) |
21 |
20
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 ) ) |
22 |
|
ustssel |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑈 ∧ ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) ) |
23 |
17 18 21 22
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) ) |
24 |
23
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) ) |
25 |
16 24
|
mpd |
⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) |