This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cff1

Description: There is always a map from ( cfA ) to A (this is a stronger condition than the definition, which only presupposes a map from some y ~( cfA ) . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cff1 ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
2 cardon ⊢ ( card ‘ 𝑦 ) ∈ On
3 eleq1 ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑥 ∈ On ↔ ( card ‘ 𝑦 ) ∈ On ) )
4 2 3 mpbiri ⊢ ( 𝑥 = ( card ‘ 𝑦 ) → 𝑥 ∈ On )
5 4 adantr ⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → 𝑥 ∈ On )
6 5 exlimiv ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → 𝑥 ∈ On )
7 6 abssi ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ⊆ On
8 cflem ⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
9 abn0 ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
10 8 9 sylibr ⊢ ( 𝐴 ∈ On → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ≠ ∅ )
11 onint ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ⊆ On ∧ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ≠ ∅ ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
12 7 10 11 sylancr ⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
13 1 12 eqeltrd ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
14 fvex ⊢ ( cf ‘ 𝐴 ) ∈ V
15 eqeq1 ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( 𝑥 = ( card ‘ 𝑦 ) ↔ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) )
16 15 anbi1d ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) ↔ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) ) )
17 16 exbidv ⊢ ( 𝑥 = ( cf ‘ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) ↔ ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) ) )
18 14 17 elab ⊢ ( ( cf ‘ 𝐴 ) ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ↔ ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
19 13 18 sylib ⊢ ( 𝐴 ∈ On → ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
20 simplr ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) )
21 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
22 sstr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On ) → 𝑦 ⊆ On )
23 21 22 sylan2 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ∈ On ) → 𝑦 ⊆ On )
24 23 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ On )
25 24 ad2ant2r ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → 𝑦 ⊆ On )
26 vex ⊢ 𝑦 ∈ V
27 onssnum ⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ⊆ On ) → 𝑦 ∈ dom card )
28 26 27 mpan ⊢ ( 𝑦 ⊆ On → 𝑦 ∈ dom card )
29 cardid2 ⊢ ( 𝑦 ∈ dom card → ( card ‘ 𝑦 ) ≈ 𝑦 )
30 28 29 syl ⊢ ( 𝑦 ⊆ On → ( card ‘ 𝑦 ) ≈ 𝑦 )
31 30 adantl ⊢ ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ 𝑦 ⊆ On ) → ( card ‘ 𝑦 ) ≈ 𝑦 )
32 breq1 ⊢ ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) → ( ( cf ‘ 𝐴 ) ≈ 𝑦 ↔ ( card ‘ 𝑦 ) ≈ 𝑦 ) )
33 32 adantr ⊢ ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ 𝑦 ⊆ On ) → ( ( cf ‘ 𝐴 ) ≈ 𝑦 ↔ ( card ‘ 𝑦 ) ≈ 𝑦 ) )
34 31 33 mpbird ⊢ ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ 𝑦 ⊆ On ) → ( cf ‘ 𝐴 ) ≈ 𝑦 )
35 bren ⊢ ( ( cf ‘ 𝐴 ) ≈ 𝑦 ↔ ∃ 𝑓 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 )
36 34 35 sylib ⊢ ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ 𝑦 ⊆ On ) → ∃ 𝑓 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 )
37 20 25 36 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ∃ 𝑓 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 )
38 f1of1 ⊢ ( 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝑦 )
39 f1ss ⊢ ( ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 )
40 39 ancoms ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝑦 ) → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 )
41 38 40 sylan2 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 )
42 41 adantlr ⊢ ( ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 )
43 42 3adant1 ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 )
44 f1ofo ⊢ ( 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 → 𝑓 : ( cf ‘ 𝐴 ) –onto→ 𝑦 )
45 foelrn ⊢ ( ( 𝑓 : ( cf ‘ 𝐴 ) –onto→ 𝑦 ∧ 𝑠 ∈ 𝑦 ) → ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑠 = ( 𝑓 ‘ 𝑤 ) )
46 sseq2 ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑤 ) → ( 𝑧 ⊆ 𝑠 ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
47 46 biimpcd ⊢ ( 𝑧 ⊆ 𝑠 → ( 𝑠 = ( 𝑓 ‘ 𝑤 ) → 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
48 47 reximdv ⊢ ( 𝑧 ⊆ 𝑠 → ( ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑠 = ( 𝑓 ‘ 𝑤 ) → ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
49 45 48 syl5com ⊢ ( ( 𝑓 : ( cf ‘ 𝐴 ) –onto→ 𝑦 ∧ 𝑠 ∈ 𝑦 ) → ( 𝑧 ⊆ 𝑠 → ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
50 49 rexlimdva ⊢ ( 𝑓 : ( cf ‘ 𝐴 ) –onto→ 𝑦 → ( ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 → ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
51 50 ralimdv ⊢ ( 𝑓 : ( cf ‘ 𝐴 ) –onto→ 𝑦 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
52 44 51 syl ⊢ ( 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
53 52 impcom ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
54 53 adantll ⊢ ( ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
55 54 3adant1 ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
56 43 55 jca ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ∧ 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 ) → ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
57 56 3expia ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ( 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 → ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) )
58 57 eximdv ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ( ∃ 𝑓 𝑓 : ( cf ‘ 𝐴 ) –1-1-onto→ 𝑦 → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) )
59 37 58 mpd ⊢ ( ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
60 59 expl ⊢ ( 𝐴 ∈ On → ( ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) )
61 60 exlimdv ⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ( ( cf ‘ 𝐴 ) = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) )
62 19 61 mpd ⊢ ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )