Metamath Proof Explorer


Theorem ac5num

Description: A version of ac5b with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion ac5num ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 uniexr ( 𝐴 ∈ dom card → 𝐴 ∈ V )
2 dfac8b ( 𝐴 ∈ dom card → ∃ 𝑟 𝑟 We 𝐴 )
3 dfac8c ( 𝐴 ∈ V → ( ∃ 𝑟 𝑟 We 𝐴 → ∃ 𝑔𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) )
4 1 2 3 sylc ( 𝐴 ∈ dom card → ∃ 𝑔𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) )
5 4 adantr ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑔𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) )
6 1 ad2antrr ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → 𝐴 ∈ V )
7 6 mptexd ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ∈ V )
8 nelne2 ( ( 𝑥𝐴 ∧ ¬ ∅ ∈ 𝐴 ) → 𝑥 ≠ ∅ )
9 8 ancoms ( ( ¬ ∅ ∈ 𝐴𝑥𝐴 ) → 𝑥 ≠ ∅ )
10 9 adantll ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ 𝑥𝐴 ) → 𝑥 ≠ ∅ )
11 pm2.27 ( 𝑥 ≠ ∅ → ( ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) → ( 𝑔𝑥 ) ∈ 𝑥 ) )
12 10 11 syl ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) → ( 𝑔𝑥 ) ∈ 𝑥 ) )
13 12 ralimdva ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ( ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) → ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝑥 ) )
14 13 imp ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝑥 )
15 fveq2 ( 𝑥 = 𝑦 → ( 𝑔𝑥 ) = ( 𝑔𝑦 ) )
16 id ( 𝑥 = 𝑦𝑥 = 𝑦 )
17 15 16 eleq12d ( 𝑥 = 𝑦 → ( ( 𝑔𝑥 ) ∈ 𝑥 ↔ ( 𝑔𝑦 ) ∈ 𝑦 ) )
18 17 rspccva ( ( ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝑥𝑦𝐴 ) → ( 𝑔𝑦 ) ∈ 𝑦 )
19 14 18 sylan ( ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ∧ 𝑦𝐴 ) → ( 𝑔𝑦 ) ∈ 𝑦 )
20 elunii ( ( ( 𝑔𝑦 ) ∈ 𝑦𝑦𝐴 ) → ( 𝑔𝑦 ) ∈ 𝐴 )
21 19 20 sylancom ( ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) ∧ 𝑦𝐴 ) → ( 𝑔𝑦 ) ∈ 𝐴 )
22 21 fmpttd ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) : 𝐴 𝐴 )
23 fveq2 ( 𝑦 = 𝑥 → ( 𝑔𝑦 ) = ( 𝑔𝑥 ) )
24 eqid ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) )
25 fvex ( 𝑔𝑥 ) ∈ V
26 23 24 25 fvmpt ( 𝑥𝐴 → ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) = ( 𝑔𝑥 ) )
27 26 eleq1d ( 𝑥𝐴 → ( ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ↔ ( 𝑔𝑥 ) ∈ 𝑥 ) )
28 27 ralbiia ( ∀ 𝑥𝐴 ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ↔ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝑥 )
29 14 28 sylibr ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥𝐴 ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 )
30 22 29 jca ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) )
31 feq1 ( 𝑓 = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) → ( 𝑓 : 𝐴 𝐴 ↔ ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) : 𝐴 𝐴 ) )
32 fveq1 ( 𝑓 = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) → ( 𝑓𝑥 ) = ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) )
33 32 eleq1d ( 𝑓 = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) → ( ( 𝑓𝑥 ) ∈ 𝑥 ↔ ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) )
34 33 ralbidv ( 𝑓 = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) → ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ↔ ∀ 𝑥𝐴 ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) )
35 31 34 anbi12d ( 𝑓 = ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) → ( ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) ↔ ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( ( 𝑦𝐴 ↦ ( 𝑔𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) ) )
36 7 30 35 spcedv ( ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥𝐴 ( 𝑥 ≠ ∅ → ( 𝑔𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )
37 5 36 exlimddv ( ( 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝑥 ) )