Metamath Proof Explorer

Theorem xpsfrnel2

Description: Elementhood in the target space of the function F appearing in xpsval . (Contributed by Mario Carneiro, 15-Aug-2015)

		Ref	Expression
	Assertion	xpsfrnel2	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpsfrnel	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) )
2		fnpr2ob	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ↔ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o )
3	2	biimpri	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
4	3	3ad2ant1	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
5		elex	⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ V )
6		elex	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ V )
7	5 6	anim12i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
8		3anass	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ) )
9		fnpr2o	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o )
10	9	biantrurd	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ) ) )
11		fvpr0o	⊢ ( 𝑋 ∈ V → ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) = 𝑋 )
12	11	eleq1d	⊢ ( 𝑋 ∈ V → ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
13		fvpr1o	⊢ ( 𝑌 ∈ V → ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) = 𝑌 )
14	13	eleq1d	⊢ ( 𝑌 ∈ V → ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ↔ 𝑌 ∈ 𝐵 ) )
15	12 14	bi2anan9	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) )
16	10 15	bitr3d	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) )
17	8 16	syl5bb	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) )
18	4 7 17	pm5.21nii	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ ∅ ) ∈ 𝐴 ∧ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 1_o ) ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
19	1 18	bitri	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )