Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Supremum and infimum
infcllem
Next ⟩
infcl
Metamath Proof Explorer
Ascii
Unicode
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