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