Metamath Proof Explorer


Theorem disjrnmpt

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 ( 𝑥𝐴𝐵 ) 𝑦 )

Proof

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 ( 𝑥𝐴𝐵 ) 𝑦 )