ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elirr GIF version

Theorem elirr 4424
Description: No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.

The reason that this theorem is marked as discouraged is a bit subtle. If we wanted to reduce usage of ax-setind 4420, we could redefine Ord 𝐴 (df-iord 4256) to also require E Fr 𝐴 (df-frind 4222) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4425 (which under that definition would presumably not need ax-setind 4420 to prove it). But since ordinals have not yet been defined that way, we cannot rely on the "don't add additional axiom use" feature of the minimizer to get theorems to use ordirr 4425. To encourage ordirr 4425 when possible, we mark this theorem as discouraged.

(Contributed by NM, 7-Aug-1994.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 26-Nov-2018.) (New usage is discouraged.)

Assertion
Ref Expression
elirr ¬ 𝐴𝐴

Proof of Theorem elirr
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neldifsnd 3622 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2 simp1 964 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴𝐴)
3 eleq1 2178 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
4 eleq1 2178 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
53, 4imbi12d 233 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
65spcgv 2745 . . . . . . . . . . . . . 14 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
76pm2.43b 52 . . . . . . . . . . . . 13 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
873ad2ant2 986 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
9 eleq2 2179 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
109imbi1d 230 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
11103ad2ant3 987 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
128, 11mpbid 146 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝐴𝐴 ∈ (V ∖ {𝐴})))
132, 12mpd 13 . . . . . . . . . 10 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14133expia 1166 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴𝐴 ∈ (V ∖ {𝐴})))
151, 14mtod 635 . . . . . . . 8 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16 vex 2661 . . . . . . . . . 10 𝑥 ∈ V
17 eldif 3048 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
1816, 17mpbiran 907 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19 velsn 3512 . . . . . . . . 9 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2018, 19xchbinx 654 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
2115, 20sylibr 133 . . . . . . 7 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
2221ex 114 . . . . . 6 (𝐴𝐴 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
2322alrimiv 1828 . . . . 5 (𝐴𝐴 → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24 df-ral 2396 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25 clelsb3 2220 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
2625imbi2i 225 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2726albii 1429 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2824, 27bitri 183 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2928imbi1i 237 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3029albii 1429 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3123, 30sylibr 133 . . . 4 (𝐴𝐴 → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32 ax-setind 4420 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
3331, 32syl 14 . . 3 (𝐴𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34 eleq1 2178 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
3534spcgv 2745 . . 3 (𝐴𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
3633, 35mpd 13 . 2 (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))
37 neldifsnd 3622 . 2 (𝐴𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
3836, 37pm2.65i 611 1 ¬ 𝐴𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  w3a 945  wal 1312   = wceq 1314  wcel 1463  [wsb 1718  wral 2391  Vcvv 2658  cdif 3036  {csn 3495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-setind 4420
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-v 2660  df-dif 3041  df-sn 3501
This theorem is referenced by:  ordirr  4425  elirrv  4431  sucprcreg  4432  ordsoexmid  4445  onnmin  4451  ssnel  4452  ordtri2or2exmid  4454  reg3exmidlemwe  4461  nntri2  6356  nntri3  6359  nndceq  6361  nndcel  6362  phpelm  6726  fiunsnnn  6741  onunsnss  6771  snon0  6790
  Copyright terms: Public domain W3C validator