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 ⊢ x ∈ On | x ≺ A ∈ On

Proof

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