Theorem inecmo

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018)

	Ref	Expression
Hypothesis	inecmo.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	inecmo	⊢ ( Rel 𝑅 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( [ 𝐵 ] 𝑅 ∩ [ 𝐶 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		inecmo.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2		ineleq	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( [ 𝐵 ] 𝑅 ∩ [ 𝐶 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) )
3		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) )
4	2 3	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( [ 𝐵 ] 𝑅 ∩ [ 𝐶 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) )
5	1	breq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 𝑅 𝑧 ↔ 𝐶 𝑅 𝑧 ) )
6	5	rmo4	⊢ ( ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) → 𝑥 = 𝑦 ) )
7		relelec	⊢ ( Rel 𝑅 → ( 𝑧 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑧 ) )
8		relelec	⊢ ( Rel 𝑅 → ( 𝑧 ∈ [ 𝐶 ] 𝑅 ↔ 𝐶 𝑅 𝑧 ) )
9	7 8	anbi12d	⊢ ( Rel 𝑅 → ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) ↔ ( 𝐵 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ) )
10	9	imbi1d	⊢ ( Rel 𝑅 → ( ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐵 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) → 𝑥 = 𝑦 ) ) )
11	10	2ralbidv	⊢ ( Rel 𝑅 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) → 𝑥 = 𝑦 ) ) )
12	6 11	bitr4id	⊢ ( Rel 𝑅 → ( ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) ) )
13	12	albidv	⊢ ( Rel 𝑅 → ( ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑧 ∈ [ 𝐵 ] 𝑅 ∧ 𝑧 ∈ [ 𝐶 ] 𝑅 ) → 𝑥 = 𝑦 ) ) )
14	4 13	bitr4id	⊢ ( Rel 𝑅 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( [ 𝐵 ] 𝑅 ∩ [ 𝐶 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ) )