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

Metamath Proof Explorer

Theorem infcllem

Description: Lemma for infcl , inflb , infglb , etc. (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 ⊢ φ → R Or A
infcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
Assertion infcllem ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z

Proof

Step Hyp Ref Expression
1 infcl.1 ⊢ φ → R Or A
2 infcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
3 vex ⊢ x ∈ V
4 vex ⊢ y ∈ V
5 3 4 brcnv ⊢ x R -1 y ↔ y R x
6 5 bicomi ⊢ y R x ↔ x R -1 y
7 6 notbii ⊢ ¬ y R x ↔ ¬ x R -1 y
8 7 ralbii ⊢ ∀ y ∈ B ¬ y R x ↔ ∀ y ∈ B ¬ x R -1 y
9 4 3 brcnv ⊢ y R -1 x ↔ x R y
10 9 bicomi ⊢ x R y ↔ y R -1 x
11 vex ⊢ z ∈ V
12 4 11 brcnv ⊢ y R -1 z ↔ z R y
13 12 bicomi ⊢ z R y ↔ y R -1 z
14 13 rexbii ⊢ ∃ z ∈ B z R y ↔ ∃ z ∈ B y R -1 z
15 10 14 imbi12i ⊢ x R y → ∃ z ∈ B z R y ↔ y R -1 x → ∃ z ∈ B y R -1 z
16 15 ralbii ⊢ ∀ y ∈ A x R y → ∃ z ∈ B z R y ↔ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
17 8 16 anbi12i ⊢ ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y ↔ ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
18 17 rexbii ⊢ ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y ↔ ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
19 2 18 sylib ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z