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

Metamath Proof Explorer

Theorem ineccnvmo

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

Ref Expression
Assertion ineccnvmo ⊢ ∀ y ∈ B ∀ z ∈ B y = z ∨ y F -1 ∩ z F -1 = ∅ ↔ ∀ x ∃* y ∈ B x F y

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ F -1
2 id ⊢ y = z → y = z
3 2 inecmo ⊢ Rel ⁡ F -1 → ∀ y ∈ B ∀ z ∈ B y = z ∨ y F -1 ∩ z F -1 = ∅ ↔ ∀ x ∃* y ∈ B y F -1 x
4 1 3 ax-mp ⊢ ∀ y ∈ B ∀ z ∈ B y = z ∨ y F -1 ∩ z F -1 = ∅ ↔ ∀ x ∃* y ∈ B y F -1 x
5 brcnvg ⊢ y ∈ V ∧ x ∈ V → y F -1 x ↔ x F y
6 5 el2v ⊢ y F -1 x ↔ x F y
7 6 rmobii ⊢ ∃* y ∈ B y F -1 x ↔ ∃* y ∈ B x F y
8 7 albii ⊢ ∀ x ∃* y ∈ B y F -1 x ↔ ∀ x ∃* y ∈ B x F y
9 4 8 bitri ⊢ ∀ y ∈ B ∀ z ∈ B y = z ∨ y F -1 ∩ z F -1 = ∅ ↔ ∀ x ∃* y ∈ B x F y