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 
|- R = ( `' O " ( _V \ 1o ) )
brwitnlem.o 
|- O Fn X
Assertion brwitnlem 
|- ( A R B <-> ( A O B ) =/= (/) )

Proof

Step Hyp Ref Expression
1 brwitnlem.r 
 |-  R = ( `' O " ( _V \ 1o ) )
2 brwitnlem.o 
 |-  O Fn X
3 fvex 
 |-  ( O ` <. A , B >. ) e. _V
4 dif1o 
 |-  ( ( O ` <. A , B >. ) e. ( _V \ 1o ) <-> ( ( O ` <. A , B >. ) e. _V /\ ( O ` <. A , B >. ) =/= (/) ) )
5 3 4 mpbiran 
 |-  ( ( O ` <. A , B >. ) e. ( _V \ 1o ) <-> ( O ` <. A , B >. ) =/= (/) )
6 5 anbi2i 
 |-  ( ( <. A , B >. e. X /\ ( O ` <. A , B >. ) e. ( _V \ 1o ) ) <-> ( <. A , B >. e. X /\ ( O ` <. A , B >. ) =/= (/) ) )
7 elpreima 
 |-  ( O Fn X -> ( <. A , B >. e. ( `' O " ( _V \ 1o ) ) <-> ( <. A , B >. e. X /\ ( O ` <. A , B >. ) e. ( _V \ 1o ) ) ) )
8 2 7 ax-mp 
 |-  ( <. A , B >. e. ( `' O " ( _V \ 1o ) ) <-> ( <. A , B >. e. X /\ ( O ` <. A , B >. ) e. ( _V \ 1o ) ) )
9 ndmfv 
 |-  ( -. <. A , B >. e. dom O -> ( O ` <. A , B >. ) = (/) )
10 9 necon1ai 
 |-  ( ( O ` <. A , B >. ) =/= (/) -> <. A , B >. e. dom O )
11 2 fndmi 
 |-  dom O = X
12 10 11 eleqtrdi 
 |-  ( ( O ` <. A , B >. ) =/= (/) -> <. A , B >. e. X )
13 12 pm4.71ri 
 |-  ( ( O ` <. A , B >. ) =/= (/) <-> ( <. A , B >. e. X /\ ( O ` <. A , B >. ) =/= (/) ) )
14 6 8 13 3bitr4i 
 |-  ( <. A , B >. e. ( `' O " ( _V \ 1o ) ) <-> ( O ` <. A , B >. ) =/= (/) )
15 1 breqi 
 |-  ( A R B <-> A ( `' O " ( _V \ 1o ) ) B )
16 df-br 
 |-  ( A ( `' O " ( _V \ 1o ) ) B <-> <. A , B >. e. ( `' O " ( _V \ 1o ) ) )
17 15 16 bitri 
 |-  ( A R B <-> <. A , B >. e. ( `' O " ( _V \ 1o ) ) )
18 df-ov 
 |-  ( A O B ) = ( O ` <. A , B >. )
19 18 neeq1i 
 |-  ( ( A O B ) =/= (/) <-> ( O ` <. A , B >. ) =/= (/) )
20 14 17 19 3bitr4i 
 |-  ( A R B <-> ( A O B ) =/= (/) )