Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cardprclem Structured version   Visualization version   GIF version

Theorem cardprclem 9384
 Description: Lemma for cardprc 9385. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
Hypothesis
Ref Expression
cardprclem.1 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥}
Assertion
Ref Expression
cardprclem ¬ 𝐴 ∈ V
Distinct variable group:   𝑥,𝐴

Proof of Theorem cardprclem
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardprclem.1 . . . . . . . . 9 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥}
21eleq2i 2903 . . . . . . . 8 (𝑥𝐴𝑥 ∈ {𝑥 ∣ (card‘𝑥) = 𝑥})
3 abid 2803 . . . . . . . 8 (𝑥 ∈ {𝑥 ∣ (card‘𝑥) = 𝑥} ↔ (card‘𝑥) = 𝑥)
4 iscard 9380 . . . . . . . 8 ((card‘𝑥) = 𝑥 ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 𝑦𝑥))
52, 3, 43bitri 300 . . . . . . 7 (𝑥𝐴 ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 𝑦𝑥))
65simplbi 501 . . . . . 6 (𝑥𝐴𝑥 ∈ On)
76ssriv 3947 . . . . 5 𝐴 ⊆ On
8 ssonuni 7476 . . . . 5 (𝐴 ∈ V → (𝐴 ⊆ On → 𝐴 ∈ On))
97, 8mpi 20 . . . 4 (𝐴 ∈ V → 𝐴 ∈ On)
10 domrefg 8519 . . . . 5 ( 𝐴 ∈ On → 𝐴 𝐴)
119, 10syl 17 . . . 4 (𝐴 ∈ V → 𝐴 𝐴)
12 elharval 9001 . . . 4 ( 𝐴 ∈ (har‘ 𝐴) ↔ ( 𝐴 ∈ On ∧ 𝐴 𝐴))
139, 11, 12sylanbrc 586 . . 3 (𝐴 ∈ V → 𝐴 ∈ (har‘ 𝐴))
147sseli 3939 . . . . . . . 8 (𝑧𝐴𝑧 ∈ On)
15 domrefg 8519 . . . . . . . . . 10 (𝑧 ∈ On → 𝑧𝑧)
1615ancli 552 . . . . . . . . 9 (𝑧 ∈ On → (𝑧 ∈ On ∧ 𝑧𝑧))
17 elharval 9001 . . . . . . . . 9 (𝑧 ∈ (har‘𝑧) ↔ (𝑧 ∈ On ∧ 𝑧𝑧))
1816, 17sylibr 237 . . . . . . . 8 (𝑧 ∈ On → 𝑧 ∈ (har‘𝑧))
1914, 18syl 17 . . . . . . 7 (𝑧𝐴𝑧 ∈ (har‘𝑧))
20 harcard 9383 . . . . . . . 8 (card‘(har‘𝑧)) = (har‘𝑧)
21 fvex 6656 . . . . . . . . 9 (har‘𝑧) ∈ V
22 fveq2 6643 . . . . . . . . . 10 (𝑥 = (har‘𝑧) → (card‘𝑥) = (card‘(har‘𝑧)))
23 id 22 . . . . . . . . . 10 (𝑥 = (har‘𝑧) → 𝑥 = (har‘𝑧))
2422, 23eqeq12d 2837 . . . . . . . . 9 (𝑥 = (har‘𝑧) → ((card‘𝑥) = 𝑥 ↔ (card‘(har‘𝑧)) = (har‘𝑧)))
2521, 24, 1elab2 3647 . . . . . . . 8 ((har‘𝑧) ∈ 𝐴 ↔ (card‘(har‘𝑧)) = (har‘𝑧))
2620, 25mpbir 234 . . . . . . 7 (har‘𝑧) ∈ 𝐴
27 eleq2 2900 . . . . . . . . 9 (𝑤 = (har‘𝑧) → (𝑧𝑤𝑧 ∈ (har‘𝑧)))
28 eleq1 2899 . . . . . . . . 9 (𝑤 = (har‘𝑧) → (𝑤𝐴 ↔ (har‘𝑧) ∈ 𝐴))
2927, 28anbi12d 633 . . . . . . . 8 (𝑤 = (har‘𝑧) → ((𝑧𝑤𝑤𝐴) ↔ (𝑧 ∈ (har‘𝑧) ∧ (har‘𝑧) ∈ 𝐴)))
3021, 29spcev 3584 . . . . . . 7 ((𝑧 ∈ (har‘𝑧) ∧ (har‘𝑧) ∈ 𝐴) → ∃𝑤(𝑧𝑤𝑤𝐴))
3119, 26, 30sylancl 589 . . . . . 6 (𝑧𝐴 → ∃𝑤(𝑧𝑤𝑤𝐴))
32 eluni 4814 . . . . . 6 (𝑧 𝐴 ↔ ∃𝑤(𝑧𝑤𝑤𝐴))
3331, 32sylibr 237 . . . . 5 (𝑧𝐴𝑧 𝐴)
3433ssriv 3947 . . . 4 𝐴 𝐴
35 harcard 9383 . . . . 5 (card‘(har‘ 𝐴)) = (har‘ 𝐴)
36 fvex 6656 . . . . . 6 (har‘ 𝐴) ∈ V
37 fveq2 6643 . . . . . . 7 (𝑥 = (har‘ 𝐴) → (card‘𝑥) = (card‘(har‘ 𝐴)))
38 id 22 . . . . . . 7 (𝑥 = (har‘ 𝐴) → 𝑥 = (har‘ 𝐴))
3937, 38eqeq12d 2837 . . . . . 6 (𝑥 = (har‘ 𝐴) → ((card‘𝑥) = 𝑥 ↔ (card‘(har‘ 𝐴)) = (har‘ 𝐴)))
4036, 39, 1elab2 3647 . . . . 5 ((har‘ 𝐴) ∈ 𝐴 ↔ (card‘(har‘ 𝐴)) = (har‘ 𝐴))
4135, 40mpbir 234 . . . 4 (har‘ 𝐴) ∈ 𝐴
4234, 41sselii 3940 . . 3 (har‘ 𝐴) ∈ 𝐴
4313, 42jctir 524 . 2 (𝐴 ∈ V → ( 𝐴 ∈ (har‘ 𝐴) ∧ (har‘ 𝐴) ∈ 𝐴))
44 eloni 6174 . . 3 ( 𝐴 ∈ On → Ord 𝐴)
45 ordn2lp 6184 . . 3 (Ord 𝐴 → ¬ ( 𝐴 ∈ (har‘ 𝐴) ∧ (har‘ 𝐴) ∈ 𝐴))
469, 44, 453syl 18 . 2 (𝐴 ∈ V → ¬ ( 𝐴 ∈ (har‘ 𝐴) ∧ (har‘ 𝐴) ∈ 𝐴))
4743, 46pm2.65i 197 1 ¬ 𝐴 ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2115  {cab 2799  ∀wral 3126  Vcvv 3471   ⊆ wss 3910  ∪ cuni 4811   class class class wbr 5039  Ord word 6163  Oncon0 6164  ‘cfv 6328   ≼ cdom 8482   ≺ csdm 8483  harchar 8996  cardccrd 9340 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-wrecs 7922  df-recs 7983  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-oi 8950  df-har 8997  df-card 9344 This theorem is referenced by:  cardprc  9385
 Copyright terms: Public domain W3C validator