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∈xy≺x
5 2 3 4 3bitri ⊢x∈A↔x∈On∧∀y∈xy≺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→∃wz∈w∧w∈A
31 19 26 30 sylancl ⊢z∈A→∃wz∈w∧w∈A
32 eluni ⊢z∈⋃A↔∃wz∈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