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

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 ⊢ 𝐴 = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
Assertion cardprclem ¬ 𝐴 ∈ V

Proof

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