| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cstucnd.3 | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝑌) | 
| 2 |  | fconst6g 6796 | . . 3
⊢ (𝐴 ∈ 𝑌 → (𝑋 × {𝐴}):𝑋⟶𝑌) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → (𝑋 × {𝐴}):𝑋⟶𝑌) | 
| 4 |  | cstucnd.1 | . . . . . 6
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 6 |  | ustne0 24223 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑉) → 𝑈 ≠ ∅) | 
| 8 |  | cstucnd.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) | 
| 9 | 8 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑉 ∈ (UnifOn‘𝑌)) | 
| 10 |  | simpllr 775 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑠 ∈ 𝑉) | 
| 11 | 1 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐴 ∈ 𝑌) | 
| 12 |  | ustref 24228 | . . . . . . . . 9
⊢ ((𝑉 ∈ (UnifOn‘𝑌) ∧ 𝑠 ∈ 𝑉 ∧ 𝐴 ∈ 𝑌) → 𝐴𝑠𝐴) | 
| 13 | 9, 10, 11, 12 | syl3anc 1372 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐴𝑠𝐴) | 
| 14 |  | simprl 770 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) | 
| 15 |  | fvconst2g 7223 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) | 
| 16 | 11, 14, 15 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑋 × {𝐴})‘𝑥) = 𝐴) | 
| 17 |  | simprr 772 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) | 
| 18 |  | fvconst2g 7223 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋) → ((𝑋 × {𝐴})‘𝑦) = 𝐴) | 
| 19 | 11, 17, 18 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑋 × {𝐴})‘𝑦) = 𝐴) | 
| 20 | 13, 16, 19 | 3brtr4d 5174 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦)) | 
| 21 | 20 | a1d 25 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))) | 
| 22 | 21 | ralrimivva 3201 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑟 ∈ 𝑈) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))) | 
| 23 | 22 | reximdva0 4354 | . . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑉) ∧ 𝑈 ≠ ∅) → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))) | 
| 24 | 7, 23 | mpdan 687 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑉) → ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))) | 
| 25 | 24 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))) | 
| 26 |  | isucn 24288 | . . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → ((𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉) ↔ ((𝑋 × {𝐴}):𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))))) | 
| 27 | 4, 8, 26 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉) ↔ ((𝑋 × {𝐴}):𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → ((𝑋 × {𝐴})‘𝑥)𝑠((𝑋 × {𝐴})‘𝑦))))) | 
| 28 | 3, 25, 27 | mpbir2and 713 | 1
⊢ (𝜑 → (𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉)) |