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 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = 𝐴 ) |