Theorem elirr 4645

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 4641, we could redefine Ord A (df-iord 4469) to also require _E Fr A (df-frind 4435) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4646 (which under that definition would presumably not need ax-setind 4641 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 4646. To encourage ordirr 4646 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 3808	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. A e. ( _V \ { A } ) )
2		simp1 1024	. . . . . . . . . . 11 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> A e. A )
3		eleq1 2294	. . . . . . . . . . . . . . . 16 |- ( y = A -> ( y e. x <-> A e. x ) )
4		eleq1 2294	. . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . 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 1046	. . . . . . . . . . . 12 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> ( A e. x -> A e. ( _V \ { A } ) ) )
9		eleq2 2295	. . . . . . . . . . . . . 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 1047	. . . . . . . . . . . 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 1232	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> ( x = A -> A e. ( _V \ { A } ) ) )
15	1, 14	mtod 669	. . . . . . . 8 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. x = A )
16		vex 2806	. . . . . . . . . 10 |- x e. _V
17		eldif 3210	. . . . . . . . . 10 |- ( x e. ( _V \ { A } ) <-> ( x e. _V /\ -. x e. { A } ) )
18	16, 17	mpbiran 949	. . . . . . . . 9 |- ( x e. ( _V \ { A } ) <-> -. x e. { A } )
19		velsn 3690	. . . . . . . . 9 |- ( x e. { A } <-> x = A )
20	18, 19	xchbinx 689	. . . . . . . 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 1922	. . . . 5 |- ( A e. A -> A. x ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
24		df-ral 2516	. . . . . . . 8 |- ( A. y e. x [ y / x ] x e. ( _V \ { A } ) <-> A. y ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) )
25		clelsb1 2336	. . . . . . . . . 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 1519	. . . . . . . 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 1519	. . . . 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 4641	. . . 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 2294	. . . 4 |- ( x = A -> ( x e. ( _V \ { A } ) <-> A e. ( _V \ { A } ) ) )
35	34	spcgv 2894	. . 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 3808	. 2 |- ( A e. A -> -. A e. ( _V \ { A } ) )
38	36, 37	pm2.65i 644	1 |- -. A e. A

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1005   A.wal 1396   = wceq 1398   [wsb 1810   e. wcel 2202   A.wral 2511   _Vcvv 2803   \ cdif 3198   {csn 3673

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-setind 4641

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-v 2805  df-dif 3203  df-sn 3679

This theorem is referenced by:  ordirr  4646  elirrv  4652  sucprcreg  4653  ordsoexmid  4666  onnmin  4672  ssnel  4673  ordtri2or2exmid  4675  reg3exmidlemwe  4683  nntri2  6705  nntri3  6708  nndceq  6710  nndcel  6711  phpelm  7096  fiunsnnn  7113  onunsnss  7152  snon0  7177