Step |
Hyp |
Ref |
Expression |
1 |
|
elrnust |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn ) |
2 |
1
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑈 ∈ ∪ ran UnifOn ) |
3 |
|
elrnust |
⊢ ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) → 𝑉 ∈ ∪ ran UnifOn ) |
4 |
3
|
adantl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑉 ∈ ∪ ran UnifOn ) |
5 |
|
ovex |
⊢ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∈ V |
6 |
5
|
rabex |
⊢ { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ∈ V |
7 |
6
|
a1i |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ∈ V ) |
8 |
|
simpr |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → 𝑣 = 𝑉 ) |
9 |
8
|
unieqd |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ∪ 𝑣 = ∪ 𝑉 ) |
10 |
9
|
dmeqd |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → dom ∪ 𝑣 = dom ∪ 𝑉 ) |
11 |
|
simpl |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → 𝑢 = 𝑈 ) |
12 |
11
|
unieqd |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ∪ 𝑢 = ∪ 𝑈 ) |
13 |
12
|
dmeqd |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → dom ∪ 𝑢 = dom ∪ 𝑈 ) |
14 |
10 13
|
oveq12d |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) = ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ) |
15 |
13
|
raleqdv |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
16 |
13 15
|
raleqbidv |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
17 |
11 16
|
rexeqbidv |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
18 |
8 17
|
raleqbidv |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
19 |
14 18
|
rabeqbidv |
⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |
20 |
|
df-ucn |
⊢ Cnu = ( 𝑢 ∈ ∪ ran UnifOn , 𝑣 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |
21 |
19 20
|
ovmpoga |
⊢ ( ( 𝑈 ∈ ∪ ran UnifOn ∧ 𝑉 ∈ ∪ ran UnifOn ∧ { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ∈ V ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |
22 |
2 4 7 21
|
syl3anc |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |
23 |
|
ustbas2 |
⊢ ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) → 𝑌 = dom ∪ 𝑉 ) |
24 |
|
ustbas2 |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 ) |
25 |
23 24
|
oveqan12rd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑌 ↑m 𝑋 ) = ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ) |
26 |
24
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑋 = dom ∪ 𝑈 ) |
27 |
26
|
raleqdv |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
28 |
26 27
|
raleqbidv |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
29 |
28
|
rexbidv |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
30 |
29
|
ralbidv |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) ) ) |
31 |
25 30
|
rabeqbidv |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( dom ∪ 𝑉 ↑m dom ∪ 𝑈 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ dom ∪ 𝑈 ∀ 𝑦 ∈ dom ∪ 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |
32 |
22 31
|
eqtr4d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } ) |