Metamath Proof Explorer

Theorem cardprclem

Description: Lemma for cardprc . (Contributed by Mario Carneiro, 22-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis cardprclem.1 ⊢ A = x | card ⁡ x = x
Assertion cardprclem ⊢ ¬ A ∈ V

Proof

Step Hyp Ref Expression
1 cardprclem.1 ⊢ A = x | card ⁡ x = x
2 1 eleq2i ⊢ x ∈ A ↔ x ∈ x | card ⁡ x = x
3 abid ⊢ x ∈ x | card ⁡ x = x ↔ card ⁡ x = x
4 iscard ⊢ card ⁡ x = x ↔ x ∈ On ∧ ∀ y ∈ x y ≺ x
5 2 3 4 3bitri ⊢ x ∈ A ↔ x ∈ On ∧ ∀ y ∈ x y ≺ x
6 5 simplbi ⊢ x ∈ A → x ∈ On
7 6 ssriv ⊢ A ⊆ On
8 ssonuni ⊢ A ∈ V → A ⊆ On → ⋃ A ∈ On
9 7 8 mpi ⊢ A ∈ V → ⋃ A ∈ On
10 domrefg ⊢ ⋃ A ∈ On → ⋃ A ≼ ⋃ A
11 9 10 syl ⊢ A ∈ V → ⋃ A ≼ ⋃ A
12 elharval ⊢ ⋃ A ∈ har ⁡ ⋃ A ↔ ⋃ A ∈ On ∧ ⋃ A ≼ ⋃ A
13 9 11 12 sylanbrc ⊢ A ∈ V → ⋃ A ∈ har ⁡ ⋃ A
14 7 sseli ⊢ z ∈ A → z ∈ On
15 domrefg ⊢ z ∈ On → z ≼ z
16 15 ancli ⊢ z ∈ On → z ∈ On ∧ z ≼ z
17 elharval ⊢ z ∈ har ⁡ z ↔ z ∈ On ∧ z ≼ z
18 16 17 sylibr ⊢ z ∈ On → z ∈ har ⁡ z
19 14 18 syl ⊢ z ∈ A → z ∈ har ⁡ z
20 harcard ⊢ card ⁡ har ⁡ z = har ⁡ z
21 fvex ⊢ har ⁡ z ∈ V
22 fveq2 ⊢ x = har ⁡ z → card ⁡ x = card ⁡ har ⁡ z
23 id ⊢ x = har ⁡ z → x = har ⁡ z
24 22 23 eqeq12d ⊢ x = har ⁡ z → card ⁡ x = x ↔ card ⁡ har ⁡ z = har ⁡ z
25 21 24 1 elab2 ⊢ har ⁡ z ∈ A ↔ card ⁡ har ⁡ z = har ⁡ z
26 20 25 mpbir ⊢ har ⁡ z ∈ A
27 eleq2 ⊢ w = har ⁡ z → z ∈ w ↔ z ∈ har ⁡ z
28 eleq1 ⊢ w = har ⁡ z → w ∈ A ↔ har ⁡ z ∈ A
29 27 28 anbi12d ⊢ w = har ⁡ z → z ∈ w ∧ w ∈ A ↔ z ∈ har ⁡ z ∧ har ⁡ z ∈ A
30 21 29 spcev ⊢ z ∈ har ⁡ z ∧ har ⁡ z ∈ A → ∃ w z ∈ w ∧ w ∈ A
31 19 26 30 sylancl ⊢ z ∈ A → ∃ w z ∈ w ∧ w ∈ A
32 eluni ⊢ z ∈ ⋃ A ↔ ∃ w z ∈ w ∧ w ∈ A
33 31 32 sylibr ⊢ z ∈ A → z ∈ ⋃ A
34 33 ssriv ⊢ A ⊆ ⋃ A
35 harcard ⊢ card ⁡ har ⁡ ⋃ A = har ⁡ ⋃ A
36 fvex ⊢ har ⁡ ⋃ A ∈ V
37 fveq2 ⊢ x = har ⁡ ⋃ A → card ⁡ x = card ⁡ har ⁡ ⋃ A
38 id ⊢ x = har ⁡ ⋃ A → x = har ⁡ ⋃ A
39 37 38 eqeq12d ⊢ x = har ⁡ ⋃ A → card ⁡ x = x ↔ card ⁡ har ⁡ ⋃ A = har ⁡ ⋃ A
40 36 39 1 elab2 ⊢ har ⁡ ⋃ A ∈ A ↔ card ⁡ har ⁡ ⋃ A = har ⁡ ⋃ A
41 35 40 mpbir ⊢ har ⁡ ⋃ A ∈ A
42 34 41 sselii ⊢ har ⁡ ⋃ A ∈ ⋃ A
43 13 42 jctir ⊢ A ∈ V → ⋃ A ∈ har ⁡ ⋃ A ∧ har ⁡ ⋃ A ∈ ⋃ A
44 eloni ⊢ ⋃ A ∈ On → Ord ⁡ ⋃ A
45 ordn2lp ⊢ Ord ⁡ ⋃ A → ¬ ⋃ A ∈ har ⁡ ⋃ A ∧ har ⁡ ⋃ A ∈ ⋃ A
46 9 44 45 3syl ⊢ A ∈ V → ¬ ⋃ A ∈ har ⁡ ⋃ A ∧ har ⁡ ⋃ A ∈ ⋃ A
47 43 46 pm2.65i ⊢ ¬ A ∈ V