Theorem disjrdx

Description: Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017)

	Ref	Expression
Hypotheses	disjrdx.1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
	disjrdx.2	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝐷 = 𝐵 )
Assertion	disjrdx	⊢ ( 𝜑 → ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		disjrdx.1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
2		disjrdx.2	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝐷 = 𝐵 )
3		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐶 → 𝐹 : 𝐴 ⟶ 𝐶 )
4	1 3	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
5	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
6		f1ofveu	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
7	1 6	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
8		eqcom	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) )
9	8	reubii	⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ∃! 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
10	7 9	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃! 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
11	2	eleq2d	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐵 ) )
12	5 10 11	rmoxfrd	⊢ ( 𝜑 → ( ∃* 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ↔ ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ) )
13	12	bicomd	⊢ ( 𝜑 → ( ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃* 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
14	13	albidv	⊢ ( 𝜑 → ( ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
15		df-disj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
16		df-disj	⊢ ( Disj 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑧 ∃* 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 )
17	14 15 16	3bitr4g	⊢ ( 𝜑 → ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷 ) )