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

Theorem ac5num 9059
 Description: A version of ac5b 9502 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.)
Assertion
Ref Expression
ac5num (( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥))
Distinct variable group:   𝑥,𝑓,𝐴

Proof of Theorem ac5num
Dummy variables 𝑔 𝑟 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniexr 7119 . . . 4 ( 𝐴 ∈ dom card → 𝐴 ∈ V)
2 dfac8b 9054 . . . 4 ( 𝐴 ∈ dom card → ∃𝑟 𝑟 We 𝐴)
3 dfac8c 9056 . . . 4 (𝐴 ∈ V → (∃𝑟 𝑟 We 𝐴 → ∃𝑔𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
41, 2, 3sylc 65 . . 3 ( 𝐴 ∈ dom card → ∃𝑔𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))
54adantr 466 . 2 (( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑔𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))
6 nelne2 3040 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ ∅ ∈ 𝐴) → 𝑥 ≠ ∅)
76ancoms 455 . . . . . . . . . . 11 ((¬ ∅ ∈ 𝐴𝑥𝐴) → 𝑥 ≠ ∅)
87adantll 693 . . . . . . . . . 10 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ 𝑥𝐴) → 𝑥 ≠ ∅)
9 pm2.27 42 . . . . . . . . . 10 (𝑥 ≠ ∅ → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) → (𝑔𝑥) ∈ 𝑥))
108, 9syl 17 . . . . . . . . 9 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ 𝑥𝐴) → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) → (𝑔𝑥) ∈ 𝑥))
1110ralimdva 3111 . . . . . . . 8 (( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → (∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) → ∀𝑥𝐴 (𝑔𝑥) ∈ 𝑥))
1211imp 393 . . . . . . 7 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∀𝑥𝐴 (𝑔𝑥) ∈ 𝑥)
13 fveq2 6332 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑔𝑥) = (𝑔𝑦))
14 id 22 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
1513, 14eleq12d 2844 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑔𝑥) ∈ 𝑥 ↔ (𝑔𝑦) ∈ 𝑦))
1615rspccva 3459 . . . . . . 7 ((∀𝑥𝐴 (𝑔𝑥) ∈ 𝑥𝑦𝐴) → (𝑔𝑦) ∈ 𝑦)
1712, 16sylan 569 . . . . . 6 (((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ∧ 𝑦𝐴) → (𝑔𝑦) ∈ 𝑦)
18 elunii 4579 . . . . . 6 (((𝑔𝑦) ∈ 𝑦𝑦𝐴) → (𝑔𝑦) ∈ 𝐴)
1917, 18sylancom 576 . . . . 5 (((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) ∧ 𝑦𝐴) → (𝑔𝑦) ∈ 𝐴)
20 eqid 2771 . . . . 5 (𝑦𝐴 ↦ (𝑔𝑦)) = (𝑦𝐴 ↦ (𝑔𝑦))
2119, 20fmptd 6527 . . . 4 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → (𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴)
221ad2antrr 705 . . . 4 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → 𝐴 ∈ V)
23 elex 3364 . . . . 5 ( 𝐴 ∈ dom card → 𝐴 ∈ V)
2423ad2antrr 705 . . . 4 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → 𝐴 ∈ V)
25 fex2 7268 . . . 4 (((𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴𝐴 ∈ V ∧ 𝐴 ∈ V) → (𝑦𝐴 ↦ (𝑔𝑦)) ∈ V)
2621, 22, 24, 25syl3anc 1476 . . 3 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → (𝑦𝐴 ↦ (𝑔𝑦)) ∈ V)
27 fveq2 6332 . . . . . . . 8 (𝑦 = 𝑥 → (𝑔𝑦) = (𝑔𝑥))
28 fvex 6342 . . . . . . . 8 (𝑔𝑥) ∈ V
2927, 20, 28fvmpt 6424 . . . . . . 7 (𝑥𝐴 → ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) = (𝑔𝑥))
3029eleq1d 2835 . . . . . 6 (𝑥𝐴 → (((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥 ↔ (𝑔𝑥) ∈ 𝑥))
3130ralbiia 3128 . . . . 5 (∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥 ↔ ∀𝑥𝐴 (𝑔𝑥) ∈ 𝑥)
3212, 31sylibr 224 . . . 4 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥)
3321, 32jca 501 . . 3 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ((𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴 ∧ ∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥))
34 feq1 6166 . . . . 5 (𝑓 = (𝑦𝐴 ↦ (𝑔𝑦)) → (𝑓:𝐴 𝐴 ↔ (𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴))
35 fveq1 6331 . . . . . . 7 (𝑓 = (𝑦𝐴 ↦ (𝑔𝑦)) → (𝑓𝑥) = ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥))
3635eleq1d 2835 . . . . . 6 (𝑓 = (𝑦𝐴 ↦ (𝑔𝑦)) → ((𝑓𝑥) ∈ 𝑥 ↔ ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥))
3736ralbidv 3135 . . . . 5 (𝑓 = (𝑦𝐴 ↦ (𝑔𝑦)) → (∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥 ↔ ∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥))
3834, 37anbi12d 616 . . . 4 (𝑓 = (𝑦𝐴 ↦ (𝑔𝑦)) → ((𝑓:𝐴 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥) ↔ ((𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴 ∧ ∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥)))
3938spcegv 3445 . . 3 ((𝑦𝐴 ↦ (𝑔𝑦)) ∈ V → (((𝑦𝐴 ↦ (𝑔𝑦)):𝐴 𝐴 ∧ ∀𝑥𝐴 ((𝑦𝐴 ↦ (𝑔𝑦))‘𝑥) ∈ 𝑥) → ∃𝑓(𝑓:𝐴 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥)))
4026, 33, 39sylc 65 . 2 ((( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) ∧ ∀𝑥𝐴 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)) → ∃𝑓(𝑓:𝐴 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥))
415, 40exlimddv 2015 1 (( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 382   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  Vcvv 3351  ∅c0 4063  ∪ cuni 4574   ↦ cmpt 4863   We wwe 5207  dom cdm 5249  ⟶wf 6027  ‘cfv 6031  cardccrd 8961 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-ord 5869  df-on 5870  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-en 8110  df-card 8965 This theorem is referenced by:  numacn  9072  ac5b  9502  ac6num  9503
 Copyright terms: Public domain W3C validator