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 
|- ( 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 ) ) )