Theorem elirr 4552

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 4548, we could redefine Ord A (df-iord 4378) to also require _E Fr A (df-frind 4344) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4553 (which under that definition would presumably not need ax-setind 4548 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 4553. To encourage ordirr 4553 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	|- -. A e. A

Proof of Theorem elirr

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neldifsnd 3735	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. A e. ( _V \ { A } ) )
2		simp1 998	. . . . . . . . . . 11 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> A e. A )
3		eleq1 2250	. . . . . . . . . . . . . . . 16 |- ( y = A -> ( y e. x <-> A e. x ) )
4		eleq1 2250	. . . . . . . . . . . . . . . 16 |- ( y = A -> ( y e. ( _V \ { A } ) <-> A e. ( _V \ { A } ) ) )
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 |- ( y = A -> ( ( y e. x -> y e. ( _V \ { A } ) ) <-> ( A e. x -> A e. ( _V \ { A } ) ) ) )
6	5	spcgv 2836	. . . . . . . . . . . . . 14 |- ( A e. x -> ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> ( A e. x -> A e. ( _V \ { A } ) ) ) )
7	6	pm2.43b 52	. . . . . . . . . . . . 13 |- ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> ( A e. x -> A e. ( _V \ { A } ) ) )
8	7	3ad2ant2 1020	. . . . . . . . . . . 12 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> ( A e. x -> A e. ( _V \ { A } ) ) )
9		eleq2 2251	. . . . . . . . . . . . . 14 |- ( x = A -> ( A e. x <-> A e. A ) )
10	9	imbi1d 231	. . . . . . . . . . . . 13 |- ( x = A -> ( ( A e. x -> A e. ( _V \ { A } ) ) <-> ( A e. A -> A e. ( _V \ { A } ) ) ) )
11	10	3ad2ant3 1021	. . . . . . . . . . . 12 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> ( ( A e. x -> A e. ( _V \ { A } ) ) <-> ( A e. A -> A e. ( _V \ { A } ) ) ) )
12	8, 11	mpbid 147	. . . . . . . . . . 11 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> ( A e. A -> A e. ( _V \ { A } ) ) )
13	2, 12	mpd 13	. . . . . . . . . 10 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> A e. ( _V \ { A } ) )
14	13	3expia 1206	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> ( x = A -> A e. ( _V \ { A } ) ) )
15	1, 14	mtod 664	. . . . . . . 8 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. x = A )
16		vex 2752	. . . . . . . . . 10 |- x e. _V
17		eldif 3150	. . . . . . . . . 10 |- ( x e. ( _V \ { A } ) <-> ( x e. _V /\ -. x e. { A } ) )
18	16, 17	mpbiran 941	. . . . . . . . 9 |- ( x e. ( _V \ { A } ) <-> -. x e. { A } )
19		velsn 3621	. . . . . . . . 9 |- ( x e. { A } <-> x = A )
20	18, 19	xchbinx 683	. . . . . . . 8 |- ( x e. ( _V \ { A } ) <-> -. x = A )
21	15, 20	sylibr 134	. . . . . . 7 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> x e. ( _V \ { A } ) )
22	21	ex 115	. . . . . 6 |- ( A e. A -> ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
23	22	alrimiv 1884	. . . . 5 |- ( A e. A -> A. x ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
24		df-ral 2470	. . . . . . . 8 |- ( A. y e. x [ y / x ] x e. ( _V \ { A } ) <-> A. y ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) )
25		clelsb1 2292	. . . . . . . . . 10 |- ( [ y / x ] x e. ( _V \ { A } ) <-> y e. ( _V \ { A } ) )
26	25	imbi2i 226	. . . . . . . . 9 |- ( ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) <-> ( y e. x -> y e. ( _V \ { A } ) ) )
27	26	albii 1480	. . . . . . . 8 |- ( A. y ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) <-> A. y ( y e. x -> y e. ( _V \ { A } ) ) )
28	24, 27	bitri 184	. . . . . . 7 |- ( A. y e. x [ y / x ] x e. ( _V \ { A } ) <-> A. y ( y e. x -> y e. ( _V \ { A } ) ) )
29	28	imbi1i 238	. . . . . 6 |- ( ( A. y e. x [ y / x ] x e. ( _V \ { A } ) -> x e. ( _V \ { A } ) ) <-> ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
30	29	albii 1480	. . . . 5 |- ( A. x ( A. y e. x [ y / x ] x e. ( _V \ { A } ) -> x e. ( _V \ { A } ) ) <-> A. x ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
31	23, 30	sylibr 134	. . . 4 |- ( A e. A -> A. x ( A. y e. x [ y / x ] x e. ( _V \ { A } ) -> x e. ( _V \ { A } ) ) )
32		ax-setind 4548	. . . 4 |- ( A. x ( A. y e. x [ y / x ] x e. ( _V \ { A } ) -> x e. ( _V \ { A } ) ) -> A. x x e. ( _V \ { A } ) )
33	31, 32	syl 14	. . 3 |- ( A e. A -> A. x x e. ( _V \ { A } ) )
34		eleq1 2250	. . . 4 |- ( x = A -> ( x e. ( _V \ { A } ) <-> A e. ( _V \ { A } ) ) )
35	34	spcgv 2836	. . 3 |- ( A e. A -> ( A. x x e. ( _V \ { A } ) -> A e. ( _V \ { A } ) ) )
36	33, 35	mpd 13	. 2 |- ( A e. A -> A e. ( _V \ { A } ) )
37		neldifsnd 3735	. 2 |- ( A e. A -> -. A e. ( _V \ { A } ) )
38	36, 37	pm2.65i 640	1 |- -. A e. A

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 979   A.wal 1361   = wceq 1363   [wsb 1772   e. wcel 2158   A.wral 2465   _Vcvv 2749   \ cdif 3138   {csn 3604

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-setind 4548

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-v 2751  df-dif 3143  df-sn 3610

This theorem is referenced by:  ordirr  4553  elirrv  4559  sucprcreg  4560  ordsoexmid  4573  onnmin  4579  ssnel  4580  ordtri2or2exmid  4582  reg3exmidlemwe  4590  nntri2  6509  nntri3  6512  nndceq  6514  nndcel  6515  phpelm  6880  fiunsnnn  6895  onunsnss  6930  snon0  6949