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

Metamath Proof Explorer

Theorem infval

Description: Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion infval ( 𝜑 → 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 supval2 ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
6 vex ⊢ 𝑥 ∈ V
7 vex ⊢ 𝑦 ∈ V
8 6 7 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
9 8 a1i ⊢ ( 𝜑 → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
10 9 notbid ⊢ ( 𝜑 → ( ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑥 ) )
11 10 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
12 7 6 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
13 12 a1i ⊢ ( 𝜑 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
14 vex ⊢ 𝑧 ∈ V
15 7 14 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
16 15 a1i ⊢ ( 𝜑 → ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 ) )
17 16 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) )
18 13 17 imbi12d ⊢ ( 𝜑 → ( ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
19 18 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
20 11 19 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
21 20 riotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
22 5 21 eqtrd ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
23 2 22 eqtrid ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )