Step |
Hyp |
Ref |
Expression |
1 |
|
infcl.1 |
⊢ ( 𝜑 → 𝑅 Or 𝐴 ) |
2 |
|
infcl.2 |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) |
3 |
|
infglbb.3 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) |
4 |
|
df-inf |
⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) |
5 |
4
|
breq1i |
⊢ ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ) |
6 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ 𝐴 ) |
7 |
|
cnvso |
⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 ) |
8 |
1 7
|
sylib |
⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 ) |
9 |
1 2
|
infcllem |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) |
10 |
8 9
|
supcl |
⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) |
11 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) |
12 |
|
brcnvg |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ) ) |
13 |
12
|
bicomd |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) ) |
14 |
6 11 13
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) ) |
15 |
8 9 3
|
suplub2 |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ↔ ∃ 𝑧 ∈ 𝐵 𝐶 ◡ 𝑅 𝑧 ) ) |
16 |
|
vex |
⊢ 𝑧 ∈ V |
17 |
|
brcnvg |
⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑧 ∈ V ) → ( 𝐶 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝐶 ) ) |
18 |
6 16 17
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝐶 ) ) |
19 |
18
|
rexbidv |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) ) |
20 |
14 15 19
|
3bitrd |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) ) |
21 |
5 20
|
syl5bb |
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) ) |