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 ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )