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