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 𝑜 if k = ∅ A B ↔ G Fn 2 𝑜 ∧ G ⁡ ∅ ∈ A ∧ G ⁡ 1 𝑜 ∈ B

Proof

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