Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpsfrnel Structured version   Visualization version   GIF version

Theorem xpsfrnel 16575
 Description: Elementhood in the target space of the function 𝐹 appearing in xpsval 16584. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
xpsfrnel (𝐺X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝐺

Proof of Theorem xpsfrnel
StepHypRef Expression
1 elixp2 8178 . 2 (𝐺X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))
2 3ancoma 1125 . . 3 ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))
3 df2o3 7839 . . . . . . . 8 2o = {∅, 1o}
43raleqi 3353 . . . . . . 7 (∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ∀𝑘 ∈ {∅, 1o} (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))
5 0ex 5013 . . . . . . . 8 ∅ ∈ V
6 1oex 7833 . . . . . . . 8 1o ∈ V
7 fveq2 6432 . . . . . . . . 9 (𝑘 = ∅ → (𝐺𝑘) = (𝐺‘∅))
8 iftrue 4311 . . . . . . . . 9 (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴)
97, 8eleq12d 2899 . . . . . . . 8 (𝑘 = ∅ → ((𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘∅) ∈ 𝐴))
10 fveq2 6432 . . . . . . . . 9 (𝑘 = 1o → (𝐺𝑘) = (𝐺‘1o))
11 1n0 7841 . . . . . . . . . . 11 1o ≠ ∅
12 neeq1 3060 . . . . . . . . . . 11 (𝑘 = 1o → (𝑘 ≠ ∅ ↔ 1o ≠ ∅))
1311, 12mpbiri 250 . . . . . . . . . 10 (𝑘 = 1o𝑘 ≠ ∅)
14 ifnefalse 4317 . . . . . . . . . 10 (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵)
1513, 14syl 17 . . . . . . . . 9 (𝑘 = 1o → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵)
1610, 15eleq12d 2899 . . . . . . . 8 (𝑘 = 1o → ((𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘1o) ∈ 𝐵))
175, 6, 9, 16ralpr 4456 . . . . . . 7 (∀𝑘 ∈ {∅, 1o} (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
184, 17bitri 267 . . . . . 6 (∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
19 2onn 7986 . . . . . . . . . 10 2o ∈ ω
20 nnfi 8421 . . . . . . . . . 10 (2o ∈ ω → 2o ∈ Fin)
2119, 20ax-mp 5 . . . . . . . . 9 2o ∈ Fin
22 fnfi 8506 . . . . . . . . 9 ((𝐺 Fn 2o ∧ 2o ∈ Fin) → 𝐺 ∈ Fin)
2321, 22mpan2 684 . . . . . . . 8 (𝐺 Fn 2o𝐺 ∈ Fin)
24 elex 3428 . . . . . . . 8 (𝐺 ∈ Fin → 𝐺 ∈ V)
2523, 24syl 17 . . . . . . 7 (𝐺 Fn 2o𝐺 ∈ V)
2625biantrurd 530 . . . . . 6 (𝐺 Fn 2o → (∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))))
2718, 26syl5rbbr 278 . . . . 5 (𝐺 Fn 2o → ((𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)))
2827pm5.32i 572 . . . 4 ((𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)))
29 3anass 1122 . . . 4 ((𝐺 Fn 2o𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))))
30 3anass 1122 . . . 4 ((𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)))
3128, 29, 303bitr4i 295 . . 3 ((𝐺 Fn 2o𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
322, 31bitri 267 . 2 ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
331, 32bitri 267 1 (𝐺X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166   ≠ wne 2998  ∀wral 3116  Vcvv 3413  ∅c0 4143  ifcif 4305  {cpr 4398   Fn wfn 6117  ‘cfv 6122  ωcom 7325  1oc1o 7818  2oc2o 7819  Xcixp 8174  Fincfn 8221 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-ral 3121  df-rex 3122  df-reu 3123  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-oadd 7829  df-er 8008  df-ixp 8175  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225 This theorem is referenced by:  xpsfrnel2  16577  xpsff1o  16580
 Copyright terms: Public domain W3C validator