This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ 𝐵 ) )