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	⊢ ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑂 𝐵 ) ≠ ∅ )