This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infglbb

Description: Bidirectional form of infglb . (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
infcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
infglbb.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion infglbb ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )

Proof

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 bitrid ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )