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

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