Metamath Proof Explorer

Theorem xpscf

Description: Equivalent condition for the pair function to be a proper function on A . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xpscf	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } : 2_o ⟶ 𝐴 ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ifid	⊢ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) = 𝐴
2	1	eleq2i	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ 𝐴 )
3	2	ralbii	⊢ ( ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ 𝐴 )
4	3	anbi2i	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ 𝐴 ) )
5		df-3an	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V ∧ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) ↔ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V ∧ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ) ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) )
6		elixp2	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V ∧ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) )
7		2onn	⊢ 2_o ∈ ω
8		fnex	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ 2_o ∈ ω ) → { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V )
9	7 8	mpan2	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o → { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V )
10	9	pm4.71ri	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V ∧ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ) )
11	10	anbi1i	⊢ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) ↔ ( ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ V ∧ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ) ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) )
12	5 6 11	3bitr4i	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ) )
13		ffnfv	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } : 2_o ⟶ 𝐴 ↔ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } Fn 2_o ∧ ∀ 𝑘 ∈ 2_o ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ‘ 𝑘 ) ∈ 𝐴 ) )
14	4 12 13	3bitr4i	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } : 2_o ⟶ 𝐴 )
15		xpsfrnel2	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } ∈ X 𝑘 ∈ 2_o if ( 𝑘 = ∅ , 𝐴 , 𝐴 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) )
16	14 15	bitr3i	⊢ ( { ⟨ ∅ , 𝑋 ⟩ , ⟨ 1_o , 𝑌 ⟩ } : 2_o ⟶ 𝐴 ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) )