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 ⊢G∈⨉k∈2𝑜ifk=∅AB↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B

Proof

Step Hyp Ref Expression
1 elixp2 ⊢G∈⨉k∈2𝑜ifk=∅AB↔G∈V∧GFn2𝑜∧∀k∈2𝑜G⁡k∈ifk=∅AB
2 3ancoma ⊢G∈V∧GFn2𝑜∧∀k∈2𝑜G⁡k∈ifk=∅AB↔GFn2𝑜∧G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB
3 2onn ⊢2𝑜∈ω
4 nnfi ⊢2𝑜∈ω→2𝑜∈Fin
5 3 4 ax-mp ⊢2𝑜∈Fin
6 fnfi ⊢GFn2𝑜∧2𝑜∈Fin→G∈Fin
7 5 6 mpan2 ⊢GFn2𝑜→G∈Fin
8 7 elexd ⊢GFn2𝑜→G∈V
9 8 biantrurd ⊢GFn2𝑜→∀k∈2𝑜G⁡k∈ifk=∅AB↔G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB
10 df2o3 ⊢2𝑜=∅1𝑜
11 10 raleqi ⊢∀k∈2𝑜G⁡k∈ifk=∅AB↔∀k∈∅1𝑜G⁡k∈ifk=∅AB
12 0ex ⊢∅∈V
13 1oex ⊢1𝑜∈V
14 fveq2 ⊢k=∅→G⁡k=G⁡∅
15 iftrue ⊢k=∅→ifk=∅AB=A
16 14 15 eleq12d ⊢k=∅→G⁡k∈ifk=∅AB↔G⁡∅∈A
17 fveq2 ⊢k=1𝑜→G⁡k=G⁡1𝑜
18 1n0 ⊢1𝑜≠∅
19 neeq1 ⊢k=1𝑜→k≠∅↔1𝑜≠∅
20 18 19 mpbiri ⊢k=1𝑜→k≠∅
21 ifnefalse ⊢k≠∅→ifk=∅AB=B
22 20 21 syl ⊢k=1𝑜→ifk=∅AB=B
23 17 22 eleq12d ⊢k=1𝑜→G⁡k∈ifk=∅AB↔G⁡1𝑜∈B
24 12 13 16 23 ralpr ⊢∀k∈∅1𝑜G⁡k∈ifk=∅AB↔G⁡∅∈A∧G⁡1𝑜∈B
25 11 24 bitri ⊢∀k∈2𝑜G⁡k∈ifk=∅AB↔G⁡∅∈A∧G⁡1𝑜∈B
26 9 25 bitr3di ⊢GFn2𝑜→G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB↔G⁡∅∈A∧G⁡1𝑜∈B
27 26 pm5.32i ⊢GFn2𝑜∧G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B
28 3anass ⊢GFn2𝑜∧G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB↔GFn2𝑜∧G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB
29 3anass ⊢GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B
30 27 28 29 3bitr4i ⊢GFn2𝑜∧G∈V∧∀k∈2𝑜G⁡k∈ifk=∅AB↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B
31 2 30 bitri ⊢G∈V∧GFn2𝑜∧∀k∈2𝑜G⁡k∈ifk=∅AB↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B
32 1 31 bitri ⊢G∈⨉k∈2𝑜ifk=∅AB↔GFn2𝑜∧G⁡∅∈A∧G⁡1𝑜∈B