# Metamath Proof Explorer

## Theorem cardf2

Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion cardf2 card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ⟶ On

### Proof

Step Hyp Ref Expression
1 df-card card = ( 𝑥 ∈ V ↦ { 𝑦 ∈ On ∣ 𝑦𝑥 } )
2 1 funmpt2 Fun card
3 rabab { 𝑥 ∈ V ∣ { 𝑦 ∈ On ∣ 𝑦𝑥 } ∈ V } = { 𝑥 { 𝑦 ∈ On ∣ 𝑦𝑥 } ∈ V }
4 1 dmmpt dom card = { 𝑥 ∈ V ∣ { 𝑦 ∈ On ∣ 𝑦𝑥 } ∈ V }
5 intexrab ( ∃ 𝑦 ∈ On 𝑦𝑥 { 𝑦 ∈ On ∣ 𝑦𝑥 } ∈ V )
6 5 abbii { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } = { 𝑥 { 𝑦 ∈ On ∣ 𝑦𝑥 } ∈ V }
7 3 4 6 3eqtr4i dom card = { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 }
8 df-fn ( card Fn { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ↔ ( Fun card ∧ dom card = { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ) )
9 2 7 8 mpbir2an card Fn { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 }
10 simpr ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } )
11 vex 𝑤 ∈ V
12 10 11 eqeltrrdi ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → { 𝑦 ∈ On ∣ 𝑦𝑧 } ∈ V )
13 intex ( { 𝑦 ∈ On ∣ 𝑦𝑧 } ≠ ∅ ↔ { 𝑦 ∈ On ∣ 𝑦𝑧 } ∈ V )
14 12 13 sylibr ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → { 𝑦 ∈ On ∣ 𝑦𝑧 } ≠ ∅ )
15 rabn0 ( { 𝑦 ∈ On ∣ 𝑦𝑧 } ≠ ∅ ↔ ∃ 𝑦 ∈ On 𝑦𝑧 )
16 14 15 sylib ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → ∃ 𝑦 ∈ On 𝑦𝑧 )
17 vex 𝑧 ∈ V
18 breq2 ( 𝑥 = 𝑧 → ( 𝑦𝑥𝑦𝑧 ) )
19 18 rexbidv ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ On 𝑦𝑥 ↔ ∃ 𝑦 ∈ On 𝑦𝑧 ) )
20 17 19 elab ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ↔ ∃ 𝑦 ∈ On 𝑦𝑧 )
21 16 20 sylibr ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } )
22 ssrab2 { 𝑦 ∈ On ∣ 𝑦𝑧 } ⊆ On
23 oninton ( ( { 𝑦 ∈ On ∣ 𝑦𝑧 } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝑦𝑧 } ≠ ∅ ) → { 𝑦 ∈ On ∣ 𝑦𝑧 } ∈ On )
24 22 14 23 sylancr ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → { 𝑦 ∈ On ∣ 𝑦𝑧 } ∈ On )
25 10 24 eqeltrd ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → 𝑤 ∈ On )
26 21 25 jca ( ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) → ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ∧ 𝑤 ∈ On ) )
27 26 ssopab2i { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) } ⊆ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ∧ 𝑤 ∈ On ) }
28 df-card card = ( 𝑧 ∈ V ↦ { 𝑦 ∈ On ∣ 𝑦𝑧 } )
29 df-mpt ( 𝑧 ∈ V ↦ { 𝑦 ∈ On ∣ 𝑦𝑧 } ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) }
30 28 29 eqtri card = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ V ∧ 𝑤 = { 𝑦 ∈ On ∣ 𝑦𝑧 } ) }
31 df-xp ( { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } × On ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ∧ 𝑤 ∈ On ) }
32 27 30 31 3sstr4i card ⊆ ( { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } × On )
33 dff2 ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ⟶ On ↔ ( card Fn { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ∧ card ⊆ ( { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } × On ) ) )
34 9 32 33 mpbir2an card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦𝑥 } ⟶ On