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

Metamath Proof Explorer

Theorem brwitnlem

Description: Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses brwitnlem.r ⊢ 𝑅 = ( ◡ 𝑂 “ ( V ∖ 1o ) )
brwitnlem.o ⊢ 𝑂 Fn 𝑋
Assertion brwitnlem ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑂 𝐵 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 brwitnlem.r ⊢ 𝑅 = ( ◡ 𝑂 “ ( V ∖ 1o ) )
2 brwitnlem.o ⊢ 𝑂 Fn 𝑋
3 fvex ⊢ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V
4 dif1o ⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( V ∖ 1o ) ↔ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
5 3 4 mpbiran ⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( V ∖ 1o ) ↔ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
6 5 anbi2i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( V ∖ 1o ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
7 elpreima ⊢ ( 𝑂 Fn 𝑋 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( V ∖ 1o ) ) ) )
8 2 7 ax-mp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( V ∖ 1o ) ) )
9 ndmfv ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝑂 → ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
10 9 necon1ai ⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝑂 )
11 2 fndmi ⊢ dom 𝑂 = 𝑋
12 10 11 eleqtrdi ⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 )
13 12 pm4.71ri ⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
14 6 8 13 3bitr4i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) ↔ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
15 1 breqi ⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( ◡ 𝑂 “ ( V ∖ 1o ) ) 𝐵 )
16 df-br ⊢ ( 𝐴 ( ◡ 𝑂 “ ( V ∖ 1o ) ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) )
17 15 16 bitri ⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) )
18 df-ov ⊢ ( 𝐴 𝑂 𝐵 ) = ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
19 18 neeq1i ⊢ ( ( 𝐴 𝑂 𝐵 ) ≠ ∅ ↔ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
20 14 17 19 3bitr4i ⊢ ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑂 𝐵 ) ≠ ∅ )