Theorem elirr 4464

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 4460, we could redefine Ord A (df-iord 4296) to also require _E Fr A (df-frind 4262) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4465 (which under that definition would presumably not need ax-setind 4460 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 4465. To encourage ordirr 4465 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 3662	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. A e. ( _V \ { A } ) )
2		simp1 982	. . . . . . . . . . 11 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> A e. A )
3		eleq1 2203	. . . . . . . . . . . . . . . 16 |- ( y = A -> ( y e. x <-> A e. x ) )
4		eleq1 2203	. . . . . . . . . . . . . . . 16 |- ( y = A -> ( y e. ( _V \ { A } ) <-> A e. ( _V \ { A } ) ) )
5	3, 4	imbi12d 233	. . . . . . . . . . . . . . 15 |- ( y = A -> ( ( y e. x -> y e. ( _V \ { A } ) ) <-> ( A e. x -> A e. ( _V \ { A } ) ) ) )
6	5	spcgv 2776	. . . . . . . . . . . . . 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 1004	. . . . . . . . . . . 12 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) /\ x = A ) -> ( A e. x -> A e. ( _V \ { A } ) ) )
9		eleq2 2204	. . . . . . . . . . . . . 14 |- ( x = A -> ( A e. x <-> A e. A ) )
10	9	imbi1d 230	. . . . . . . . . . . . 13 |- ( x = A -> ( ( A e. x -> A e. ( _V \ { A } ) ) <-> ( A e. A -> A e. ( _V \ { A } ) ) ) )
11	10	3ad2ant3 1005	. . . . . . . . . . . 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 146	. . . . . . . . . . 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 1184	. . . . . . . . 9 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> ( x = A -> A e. ( _V \ { A } ) ) )
15	1, 14	mtod 653	. . . . . . . 8 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> -. x = A )
16		vex 2692	. . . . . . . . . 10 |- x e. _V
17		eldif 3085	. . . . . . . . . 10 |- ( x e. ( _V \ { A } ) <-> ( x e. _V /\ -. x e. { A } ) )
18	16, 17	mpbiran 925	. . . . . . . . 9 |- ( x e. ( _V \ { A } ) <-> -. x e. { A } )
19		velsn 3549	. . . . . . . . 9 |- ( x e. { A } <-> x = A )
20	18, 19	xchbinx 672	. . . . . . . 8 |- ( x e. ( _V \ { A } ) <-> -. x = A )
21	15, 20	sylibr 133	. . . . . . 7 |- ( ( A e. A /\ A. y ( y e. x -> y e. ( _V \ { A } ) ) ) -> x e. ( _V \ { A } ) )
22	21	ex 114	. . . . . 6 |- ( A e. A -> ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
23	22	alrimiv 1847	. . . . 5 |- ( A e. A -> A. x ( A. y ( y e. x -> y e. ( _V \ { A } ) ) -> x e. ( _V \ { A } ) ) )
24		df-ral 2422	. . . . . . . 8 |- ( A. y e. x [ y / x ] x e. ( _V \ { A } ) <-> A. y ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) )
25		clelsb3 2245	. . . . . . . . . 10 |- ( [ y / x ] x e. ( _V \ { A } ) <-> y e. ( _V \ { A } ) )
26	25	imbi2i 225	. . . . . . . . 9 |- ( ( y e. x -> [ y / x ] x e. ( _V \ { A } ) ) <-> ( y e. x -> y e. ( _V \ { A } ) ) )
27	26	albii 1447	. . . . . . . 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 183	. . . . . . 7 |- ( A. y e. x [ y / x ] x e. ( _V \ { A } ) <-> A. y ( y e. x -> y e. ( _V \ { A } ) ) )
29	28	imbi1i 237	. . . . . 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 1447	. . . . 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 133	. . . 4 |- ( A e. A -> A. x ( A. y e. x [ y / x ] x e. ( _V \ { A } ) -> x e. ( _V \ { A } ) ) )
32		ax-setind 4460	. . . 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 2203	. . . 4 |- ( x = A -> ( x e. ( _V \ { A } ) <-> A e. ( _V \ { A } ) ) )
35	34	spcgv 2776	. . 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 3662	. 2 |- ( A e. A -> -. A e. ( _V \ { A } ) )
38	36, 37	pm2.65i 629	1 |- -. A e. A

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 963   A.wal 1330   = wceq 1332   e. wcel 1481   [wsb 1736   A.wral 2417   _Vcvv 2689   \ cdif 3073   {csn 3532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-setind 4460

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-v 2691  df-dif 3078  df-sn 3538

This theorem is referenced by:  ordirr  4465  elirrv  4471  sucprcreg  4472  ordsoexmid  4485  onnmin  4491  ssnel  4492  ordtri2or2exmid  4494  reg3exmidlemwe  4501  nntri2  6398  nntri3  6401  nndceq  6403  nndcel  6404  phpelm  6768  fiunsnnn  6783  onunsnss  6813  snon0  6832