Metamath Proof Explorer


Theorem infcllem

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

Ref Expression
Hypotheses infcl.1
|- ( ph -> R Or A )
infcl.2
|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion infcllem
|- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )

Proof

Step Hyp Ref Expression
1 infcl.1
 |-  ( ph -> R Or A )
2 infcl.2
 |-  ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
3 vex
 |-  x e. _V
4 vex
 |-  y e. _V
5 3 4 brcnv
 |-  ( x `' R y <-> y R x )
6 5 bicomi
 |-  ( y R x <-> x `' R y )
7 6 notbii
 |-  ( -. y R x <-> -. x `' R y )
8 7 ralbii
 |-  ( A. y e. B -. y R x <-> A. y e. B -. x `' R y )
9 4 3 brcnv
 |-  ( y `' R x <-> x R y )
10 9 bicomi
 |-  ( x R y <-> y `' R x )
11 vex
 |-  z e. _V
12 4 11 brcnv
 |-  ( y `' R z <-> z R y )
13 12 bicomi
 |-  ( z R y <-> y `' R z )
14 13 rexbii
 |-  ( E. z e. B z R y <-> E. z e. B y `' R z )
15 10 14 imbi12i
 |-  ( ( x R y -> E. z e. B z R y ) <-> ( y `' R x -> E. z e. B y `' R z ) )
16 15 ralbii
 |-  ( A. y e. A ( x R y -> E. z e. B z R y ) <-> A. y e. A ( y `' R x -> E. z e. B y `' R z ) )
17 8 16 anbi12i
 |-  ( ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
18 17 rexbii
 |-  ( E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
19 2 18 sylib
 |-  ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )