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