Metamath Proof Explorer

Theorem axccdom

Description: Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses axccdom.1 ⊢ ( 𝜑 → 𝑋 ≼ ω )
axccdom.2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ≠ ∅ )
Assertion axccdom ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 axccdom.1 ⊢ ( 𝜑 → 𝑋 ≼ ω )
2 axccdom.2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ≠ ∅ )
3 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Fin ) → 𝑋 ∈ Fin )
4 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Fin ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
5 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Fin ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ≠ ∅ )
6 3 4 5 choicefi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Fin ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ Fin ) → 𝑋 ≼ ω )
8 isfinite2 ⊢ ( 𝑋 ≺ ω → 𝑋 ∈ Fin )
9 8 con3i ⊢ ( ¬ 𝑋 ∈ Fin → ¬ 𝑋 ≺ ω )
10 9 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ Fin ) → ¬ 𝑋 ≺ ω )
11 7 10 jca ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ Fin ) → ( 𝑋 ≼ ω ∧ ¬ 𝑋 ≺ ω ) )
12 bren2 ⊢ ( 𝑋 ≈ ω ↔ ( 𝑋 ≼ ω ∧ ¬ 𝑋 ≺ ω ) )
13 11 12 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ Fin ) → 𝑋 ≈ ω )
14 ctex ⊢ ( 𝑋 ≼ ω → 𝑋 ∈ V )
15 1 14 syl ⊢ ( 𝜑 → 𝑋 ∈ V )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → 𝑋 ∈ V )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → 𝑋 ≈ ω )
18 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≈ ω ↔ 𝑋 ≈ ω ) )
19 raleq ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) )
20 19 exbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑔 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) )
21 18 20 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( 𝑋 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ) )
22 ax-cc ⊢ ( 𝑥 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
23 21 22 vtoclg ⊢ ( 𝑋 ∈ V → ( 𝑋 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) )
24 16 17 23 sylc ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → ∃ 𝑔 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
25 15 mptexd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ∈ V )
26 25 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ∈ V )
27 fvex ⊢ ( 𝑔 ‘ 𝑧 ) ∈ V
28 27 rgenw ⊢ ∀ 𝑧 ∈ 𝑋 ( 𝑔 ‘ 𝑧 ) ∈ V
29 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) )
30 29 fnmpt ⊢ ( ∀ 𝑧 ∈ 𝑋 ( 𝑔 ‘ 𝑧 ) ∈ V → ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 )
31 28 30 ax-mp ⊢ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋
32 31 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 )
33 nfv ⊢ Ⅎ 𝑧 𝜑
34 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 )
35 33 34 nfan ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
36 id ⊢ ( 𝑧 ∈ 𝑋 → 𝑧 ∈ 𝑋 )
37 27 a1i ⊢ ( 𝑧 ∈ 𝑋 → ( 𝑔 ‘ 𝑧 ) ∈ V )
38 29 fvmpt2 ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝑧 ) ∈ V ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
39 36 37 38 syl2anc ⊢ ( 𝑧 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
41 rspa ⊢ ( ( ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
42 41 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
43 2 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ≠ ∅ )
44 id ⊢ ( ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )
45 42 43 44 sylc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 )
46 40 45 eqeltrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 )
47 46 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑧 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
48 35 47 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 )
49 32 48 jca ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
50 fneq1 ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) → ( 𝑓 Fn 𝑋 ↔ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 ) )
51 nfcv ⊢ Ⅎ 𝑧 𝑓
52 nfmpt1 ⊢ Ⅎ 𝑧 ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) )
53 51 52 nfeq ⊢ Ⅎ 𝑧 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) )
54 fveq1 ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) → ( 𝑓 ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) )
55 54 eleq1d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
56 53 55 ralbid ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) )
57 50 56 anbi12d ⊢ ( 𝑓 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) → ( ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
58 57 spcegv ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ∈ V → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑧 ) ) ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
59 26 49 58 sylc ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≈ ω ) ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
61 60 ex ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → ( ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
62 61 exlimdv ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → ( ∃ 𝑔 ∀ 𝑧 ∈ 𝑋 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
63 24 62 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ≈ ω ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
64 13 63 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ Fin ) → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
65 6 64 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )