Theorem xpsfrnel

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

	Ref	Expression
Assertion	xpsfrnel	⊢ ( 𝐺 ∈ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 Fn 2o ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elixp2	⊢ ( 𝐺 ∈ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) )
2		3ancoma	⊢ ( ( 𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ↔ ( 𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) )
3		2onn	⊢ 2o ∈ ω
4		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
5	3 4	ax-mp	⊢ 2o ∈ Fin
6		fnfi	⊢ ( ( 𝐺 Fn 2o ∧ 2o ∈ Fin ) → 𝐺 ∈ Fin )
7	5 6	mpan2	⊢ ( 𝐺 Fn 2o → 𝐺 ∈ Fin )
8	7	elexd	⊢ ( 𝐺 Fn 2o → 𝐺 ∈ V )
9	8	biantrurd	⊢ ( 𝐺 Fn 2o → ( ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ) )
10		df2o3	⊢ 2o = { ∅ , 1o }
11	10	raleqi	⊢ ( ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ∀ 𝑘 ∈ { ∅ , 1o } ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) )
12		0ex	⊢ ∅ ∈ V
13		1oex	⊢ 1o ∈ V
14		fveq2	⊢ ( 𝑘 = ∅ → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ∅ ) )
15		iftrue	⊢ ( 𝑘 = ∅ → if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) = 𝐴 )
16	14 15	eleq12d	⊢ ( 𝑘 = ∅ → ( ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ) )
17		fveq2	⊢ ( 𝑘 = 1o → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 1o ) )
18		1n0	⊢ 1o ≠ ∅
19		neeq1	⊢ ( 𝑘 = 1o → ( 𝑘 ≠ ∅ ↔ 1o ≠ ∅ ) )
20	18 19	mpbiri	⊢ ( 𝑘 = 1o → 𝑘 ≠ ∅ )
21		ifnefalse	⊢ ( 𝑘 ≠ ∅ → if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) = 𝐵 )
22	20 21	syl	⊢ ( 𝑘 = 1o → if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) = 𝐵 )
23	17 22	eleq12d	⊢ ( 𝑘 = 1o → ( ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )
24	12 13 16 23	ralpr	⊢ ( ∀ 𝑘 ∈ { ∅ , 1o } ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )
25	11 24	bitri	⊢ ( ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )
26	9 25	bitr3di	⊢ ( 𝐺 Fn 2o → ( ( 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ↔ ( ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) ) )
27	26	pm5.32i	⊢ ( ( 𝐺 Fn 2o ∧ ( 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ) ↔ ( 𝐺 Fn 2o ∧ ( ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) ) )
28		3anass	⊢ ( ( 𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ↔ ( 𝐺 Fn 2o ∧ ( 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ) )
29		3anass	⊢ ( ( 𝐺 Fn 2o ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) ↔ ( 𝐺 Fn 2o ∧ ( ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) ) )
30	27 28 29	3bitr4i	⊢ ( ( 𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ↔ ( 𝐺 Fn 2o ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )
31	2 30	bitri	⊢ ( ( 𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀ 𝑘 ∈ 2o ( 𝐺 ‘ 𝑘 ) ∈ if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ) ↔ ( 𝐺 Fn 2o ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )
32	1 31	bitri	⊢ ( 𝐺 ∈ X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝐴 , 𝐵 ) ↔ ( 𝐺 Fn 2o ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ∧ ( 𝐺 ‘ 1o ) ∈ 𝐵 ) )