Description: Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | disjrnmpt | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjabrex | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 ) | |
2 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
3 | 2 | rnmpt | ⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } |
4 | disjeq1 | ⊢ ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } → ( Disj 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ↔ Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 ) ) | |
5 | 3 4 | ax-mp | ⊢ ( Disj 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ↔ Disj 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } 𝑦 ) |
6 | 1 5 | sylibr | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) |