Theorem card2on

Description: The alternate definition of the cardinal of a set given in cardval2 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013)

	Ref	Expression
Assertion	card2on	⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On

Proof

Step	Hyp	Ref	Expression
1		onelon	⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ∈ On )
2		vex	⊢ 𝑧 ∈ V
3		onelss	⊢ ( 𝑧 ∈ On → ( 𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧 ) )
4	3	imp	⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ⊆ 𝑧 )
5		ssdomg	⊢ ( 𝑧 ∈ V → ( 𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧 ) )
6	2 4 5	mpsyl	⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → 𝑦 ≼ 𝑧 )
7	1 6	jca	⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) → ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝑧 ) )
8		domsdomtr	⊢ ( ( 𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴 ) → 𝑦 ≺ 𝐴 )
9	8	anim2i	⊢ ( ( 𝑦 ∈ On ∧ ( 𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴 ) ) → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) )
10	9	anassrs	⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝑧 ) ∧ 𝑧 ≺ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) )
11	7 10	sylan	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑧 ≺ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) )
12	11	exp31	⊢ ( 𝑧 ∈ On → ( 𝑦 ∈ 𝑧 → ( 𝑧 ≺ 𝐴 → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) ) ) )
13	12	com12	⊢ ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ On → ( 𝑧 ≺ 𝐴 → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) ) ) )
14	13	impd	⊢ ( 𝑦 ∈ 𝑧 → ( ( 𝑧 ∈ On ∧ 𝑧 ≺ 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) ) )
15		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴 ) )
16	15	elrab	⊢ ( 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ↔ ( 𝑧 ∈ On ∧ 𝑧 ≺ 𝐴 ) )
17		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≺ 𝐴 ↔ 𝑦 ≺ 𝐴 ) )
18	17	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ↔ ( 𝑦 ∈ On ∧ 𝑦 ≺ 𝐴 ) )
19	14 16 18	3imtr4g	⊢ ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) )
20	19	imp	⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )
21	20	gen2	⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )
22		dftr2	⊢ ( Tr { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) → 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) )
23	21 22	mpbir	⊢ Tr { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 }
24		ssrab2	⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ⊆ On
25		ordon	⊢ Ord On
26		trssord	⊢ ( ( Tr { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∧ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ⊆ On ∧ Ord On ) → Ord { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )
27	23 24 25 26	mp3an	⊢ Ord { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 }
28		hartogs	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On )
29		sdomdom	⊢ ( 𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴 )
30	29	a1i	⊢ ( 𝑥 ∈ On → ( 𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴 ) )
31	30	ss2rabi	⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ⊆ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 }
32		ssexg	⊢ ( ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ⊆ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∧ { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On ) → { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ V )
33	31 32	mpan	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ V )
34		elong	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ V → ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) )
35	28 33 34	3syl	⊢ ( 𝐴 ∈ V → ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On ↔ Ord { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ) )
36	27 35	mpbiri	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On )
37		0elon	⊢ ∅ ∈ On
38		eleq1	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = ∅ → ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On ↔ ∅ ∈ On ) )
39	37 38	mpbiri	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = ∅ → { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On )
40		df-ne	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ≠ ∅ ↔ ¬ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = ∅ )
41		rabn0	⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝑥 ≺ 𝐴 )
42	40 41	bitr3i	⊢ ( ¬ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = ∅ ↔ ∃ 𝑥 ∈ On 𝑥 ≺ 𝐴 )
43		relsdom	⊢ Rel ≺
44	43	brrelex2i	⊢ ( 𝑥 ≺ 𝐴 → 𝐴 ∈ V )
45	44	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝑥 ≺ 𝐴 → 𝐴 ∈ V )
46	42 45	sylbi	⊢ ( ¬ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = ∅ → 𝐴 ∈ V )
47	39 46	nsyl4	⊢ ( ¬ 𝐴 ∈ V → { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On )
48	36 47	pm2.61i	⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ∈ On