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		fndm	⊢ ( 𝑂 Fn 𝑋 → dom 𝑂 = 𝑋 )
12	2 11	ax-mp	⊢ dom 𝑂 = 𝑋
13	10 12	eleqtrdi	⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 )
14	13	pm4.71ri	⊢ ( ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑋 ∧ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
15	6 8 14	3bitr4i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) ↔ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
16	1	breqi	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( ◡ 𝑂 “ ( V ∖ 1o ) ) 𝐵 )
17		df-br	⊢ ( 𝐴 ( ◡ 𝑂 “ ( V ∖ 1o ) ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) )
18	16 17	bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ 𝑂 “ ( V ∖ 1o ) ) )
19		df-ov	⊢ ( 𝐴 𝑂 𝐵 ) = ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
20	19	neeq1i	⊢ ( ( 𝐴 𝑂 𝐵 ) ≠ ∅ ↔ ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
21	15 18 20	3bitr4i	⊢ ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑂 𝐵 ) ≠ ∅ )