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

Metamath Proof Explorer

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