Description: Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dmdju.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ ) | |
| Assertion | dmdju | ⊢ ( 𝜑 → dom ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmdju.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ ) | |
| 2 | dmiun | ⊢ dom ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 dom ( { 𝑥 } × 𝐵 ) | |
| 3 | dmxp | ⊢ ( 𝐵 ≠ ∅ → dom ( { 𝑥 } × 𝐵 ) = { 𝑥 } ) | |
| 4 | 1 3 | syl | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom ( { 𝑥 } × 𝐵 ) = { 𝑥 } ) |
| 5 | 4 | iuneq2dv | ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 dom ( { 𝑥 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) |
| 6 | 2 5 | eqtrid | ⊢ ( 𝜑 → dom ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) |
| 7 | iunid | ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴 | |
| 8 | 6 7 | eqtrdi | ⊢ ( 𝜑 → dom ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = 𝐴 ) |