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

Theorem elirr 4266
 Description: No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 26-Nov-2018.)
Assertion
Ref Expression
elirr ¬ 𝐴𝐴

Proof of Theorem elirr
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neldifsnd 3498 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2 simp1 904 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴𝐴)
3 eleq1 2100 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
4 eleq1 2100 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
53, 4imbi12d 223 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
65spcgv 2640 . . . . . . . . . . . . . 14 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
76pm2.43b 46 . . . . . . . . . . . . 13 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
873ad2ant2 926 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
9 eleq2 2101 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
109imbi1d 220 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
11103ad2ant3 927 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
128, 11mpbid 135 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝐴𝐴 ∈ (V ∖ {𝐴})))
132, 12mpd 13 . . . . . . . . . 10 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14133expia 1106 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴𝐴 ∈ (V ∖ {𝐴})))
151, 14mtod 589 . . . . . . . 8 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16 vex 2560 . . . . . . . . . 10 𝑥 ∈ V
17 eldif 2927 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
1816, 17mpbiran 847 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19 velsn 3392 . . . . . . . . 9 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2018, 19xchbinx 607 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
2115, 20sylibr 137 . . . . . . 7 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
2221ex 108 . . . . . 6 (𝐴𝐴 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
2322alrimiv 1754 . . . . 5 (𝐴𝐴 → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24 df-ral 2311 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25 clelsb3 2142 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
2625imbi2i 215 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2726albii 1359 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2824, 27bitri 173 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2928imbi1i 227 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3029albii 1359 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3123, 30sylibr 137 . . . 4 (𝐴𝐴 → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32 ax-setind 4262 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
3331, 32syl 14 . . 3 (𝐴𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34 eleq1 2100 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
3534spcgv 2640 . . 3 (𝐴𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
3633, 35mpd 13 . 2 (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))
37 neldifsnd 3498 . 2 (𝐴𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
3836, 37pm2.65i 568 1 ¬ 𝐴𝐴
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885  ∀wal 1241   = wceq 1243   ∈ wcel 1393  [wsb 1645  ∀wral 2306  Vcvv 2557   ∖ cdif 2914  {csn 3375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-setind 4262 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-v 2559  df-dif 2920  df-sn 3381 This theorem is referenced by:  ordirr  4267  elirrv  4272  sucprcreg  4273  dtruex  4283  ordsoexmid  4286  onnmin  4292  ssnel  4293  onpsssuc  4295  ordtri2or2exmid  4296  reg3exmidlemwe  4303  nntri2  6073  nntri3  6075  nndceq  6077  nndcel  6078  phpelm  6328  fiunsnnn  6338  onunsnss  6355  snon0  6356
 Copyright terms: Public domain W3C validator