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

Theorem elirr 4347
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 4343, we could redefine Ord 𝐴 (df-iord 4184) to also require E Fr 𝐴 (df-frind 4150) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4348 (which under that definition would presumably not need ax-setind 4343 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 4348. To encourage ordirr 4348 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 3566 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2 simp1 943 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴𝐴)
3 eleq1 2150 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
4 eleq1 2150 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
53, 4imbi12d 232 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
65spcgv 2706 . . . . . . . . . . . . . 14 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
76pm2.43b 51 . . . . . . . . . . . . 13 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
873ad2ant2 965 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
9 eleq2 2151 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
109imbi1d 229 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
11103ad2ant3 966 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
128, 11mpbid 145 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝐴𝐴 ∈ (V ∖ {𝐴})))
132, 12mpd 13 . . . . . . . . . 10 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14133expia 1145 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴𝐴 ∈ (V ∖ {𝐴})))
151, 14mtod 624 . . . . . . . 8 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16 vex 2622 . . . . . . . . . 10 𝑥 ∈ V
17 eldif 3006 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
1816, 17mpbiran 886 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19 velsn 3458 . . . . . . . . 9 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2018, 19xchbinx 642 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
2115, 20sylibr 132 . . . . . . 7 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
2221ex 113 . . . . . 6 (𝐴𝐴 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
2322alrimiv 1802 . . . . 5 (𝐴𝐴 → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24 df-ral 2364 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25 clelsb3 2192 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
2625imbi2i 224 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2726albii 1404 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2824, 27bitri 182 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2928imbi1i 236 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3029albii 1404 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3123, 30sylibr 132 . . . 4 (𝐴𝐴 → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32 ax-setind 4343 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
3331, 32syl 14 . . 3 (𝐴𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34 eleq1 2150 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
3534spcgv 2706 . . 3 (𝐴𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
3633, 35mpd 13 . 2 (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))
37 neldifsnd 3566 . 2 (𝐴𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
3836, 37pm2.65i 603 1 ¬ 𝐴𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  w3a 924  wal 1287   = wceq 1289  wcel 1438  [wsb 1692  wral 2359  Vcvv 2619  cdif 2994  {csn 3441
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-setind 4343
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-v 2621  df-dif 2999  df-sn 3447
This theorem is referenced by:  ordirr  4348  elirrv  4354  sucprcreg  4355  ordsoexmid  4368  onnmin  4374  ssnel  4375  ordtri2or2exmid  4377  reg3exmidlemwe  4384  nntri2  6237  nntri3  6240  nndceq  6242  nndcel  6243  phpelm  6562  fiunsnnn  6577  onunsnss  6607  snon0  6624
  Copyright terms: Public domain W3C validator