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

Theorem elirr 4540
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 4536, we could redefine Ord 𝐴 (df-iord 4366) to also require E Fr 𝐴 (df-frind 4332) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4541 (which under that definition would presumably not need ax-setind 4536 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 4541. To encourage ordirr 4541 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 3723 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2 simp1 997 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴𝐴)
3 eleq1 2240 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
4 eleq1 2240 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
53, 4imbi12d 234 . . . . . . . . . . . . . . 15 (𝑦 = 𝐴 → ((𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
65spcgv 2824 . . . . . . . . . . . . . 14 (𝐴𝑥 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴}))))
76pm2.43b 52 . . . . . . . . . . . . 13 (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
873ad2ant2 1019 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝑥𝐴 ∈ (V ∖ {𝐴})))
9 eleq2 2241 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
109imbi1d 231 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
11103ad2ant3 1020 . . . . . . . . . . . 12 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴𝑥𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))))
128, 11mpbid 147 . . . . . . . . . . 11 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴𝐴𝐴 ∈ (V ∖ {𝐴})))
132, 12mpd 13 . . . . . . . . . 10 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14133expia 1205 . . . . . . . . 9 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴𝐴 ∈ (V ∖ {𝐴})))
151, 14mtod 663 . . . . . . . 8 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16 vex 2740 . . . . . . . . . 10 𝑥 ∈ V
17 eldif 3138 . . . . . . . . . 10 (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
1816, 17mpbiran 940 . . . . . . . . 9 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19 velsn 3609 . . . . . . . . 9 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2018, 19xchbinx 682 . . . . . . . 8 (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
2115, 20sylibr 134 . . . . . . 7 ((𝐴𝐴 ∧ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
2221ex 115 . . . . . 6 (𝐴𝐴 → (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
2322alrimiv 1874 . . . . 5 (𝐴𝐴 → ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24 df-ral 2460 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25 clelsb1 2282 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
2625imbi2i 226 . . . . . . . . 9 ((𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2726albii 1470 . . . . . . . 8 (∀𝑦(𝑦𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2824, 27bitri 184 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})))
2928imbi1i 238 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3029albii 1470 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦𝑥𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
3123, 30sylibr 134 . . . 4 (𝐴𝐴 → ∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32 ax-setind 4536 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
3331, 32syl 14 . . 3 (𝐴𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34 eleq1 2240 . . . 4 (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
3534spcgv 2824 . . 3 (𝐴𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
3633, 35mpd 13 . 2 (𝐴𝐴𝐴 ∈ (V ∖ {𝐴}))
37 neldifsnd 3723 . 2 (𝐴𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
3836, 37pm2.65i 639 1 ¬ 𝐴𝐴
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  w3a 978  wal 1351   = wceq 1353  [wsb 1762  wcel 2148  wral 2455  Vcvv 2737  cdif 3126  {csn 3592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-setind 4536
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-v 2739  df-dif 3131  df-sn 3598
This theorem is referenced by:  ordirr  4541  elirrv  4547  sucprcreg  4548  ordsoexmid  4561  onnmin  4567  ssnel  4568  ordtri2or2exmid  4570  reg3exmidlemwe  4578  nntri2  6494  nntri3  6497  nndceq  6499  nndcel  6500  phpelm  6865  fiunsnnn  6880  onunsnss  6915  snon0  6934
  Copyright terms: Public domain W3C validator