This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( [ 𝐵 ] 𝑅 ∩ [ 𝐶 ] 𝑅 ) = ∅ ) ↔ ∀ 𝑧 ∃* 𝑥 ∈ 𝐴 𝐵 𝑅 𝑧 ) )