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