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

Metamath Proof Explorer

Theorem eqinf

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion eqinf ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 infexd.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 df-inf ⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
3 cnvso ⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
4 1 3 sylib ⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
5 4 eqsup ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = 𝐶 ) )
6 brcnvg ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V ) → ( 𝐶 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝐶 ) )
7 6 bicomd ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑦 ∈ V ) → ( 𝑦 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑦 ) )
8 7 elvd ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑦 ) )
9 8 notbid ⊢ ( 𝐶 ∈ 𝐴 → ( ¬ 𝑦 𝑅 𝐶 ↔ ¬ 𝐶 ◡ 𝑅 𝑦 ) )
10 9 ralbidv ⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ) )
11 vex ⊢ 𝑦 ∈ V
12 brcnvg ⊢ ( ( 𝑦 ∈ V ∧ 𝐶 ∈ 𝐴 ) → ( 𝑦 ◡ 𝑅 𝐶 ↔ 𝐶 𝑅 𝑦 ) )
13 11 12 mpan ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 ◡ 𝑅 𝐶 ↔ 𝐶 𝑅 𝑦 ) )
14 13 bicomd ⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 𝑅 𝑦 ↔ 𝑦 ◡ 𝑅 𝐶 ) )
15 vex ⊢ 𝑧 ∈ V
16 11 15 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
17 16 a1i ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 ) )
18 17 bicomd ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑧 𝑅 𝑦 ↔ 𝑦 ◡ 𝑅 𝑧 ) )
19 18 rexbidv ⊢ ( 𝐶 ∈ 𝐴 → ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) )
20 14 19 imbi12d ⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
21 20 ralbidv ⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
22 10 21 anbi12d ⊢ ( 𝐶 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
23 22 pm5.32i ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
24 3anass ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
25 3anass ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
26 23 24 25 3bitr4i ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
27 26 biimpi ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
28 5 27 impel ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = 𝐶 )
29 2 28 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )
30 29 ex ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝐶 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝐶 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )