Theorem elirr 4633

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 4629, we could redefine Ord 𝐴 (df-iord 4457) to also require E Fr 𝐴 (df-frind 4423) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4634 (which under that definition would presumably not need ax-setind 4629 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 4634. To encourage ordirr 4634 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.

Step	Hyp	Ref	Expression
1		neldifsnd 3799	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2		simp1 1021	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝐴)
3		eleq1 2292	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
4		eleq1 2292	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
6	5	spcgv 2890	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑥 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
7	6	pm2.43b 52	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
8	7	3ad2ant2 1043	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
9		eleq2 2293	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴))
10	9	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
11	10	3ad2ant3 1044	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
12	8, 11	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
13	2, 12	mpd 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14	13	3expia 1229	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
15	1, 14	mtod 667	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16		vex 2802	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		eldif 3206	. . . . . . . . . 10 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
18	16, 17	mpbiran 946	. . . . . . . . 9 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19		velsn 3683	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
20	18, 19	xchbinx 686	. . . . . . . 8 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
21	15, 20	sylibr 134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
22	21	ex 115	. . . . . 6 ⊢ (𝐴 ∈ 𝐴 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
23	22	alrimiv 1920	. . . . 5 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24		df-ral 2513	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25		clelsb1 2334	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
26	25	imbi2i 226	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
27	26	albii 1516	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
28	24, 27	bitri 184	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
29	28	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
30	29	albii 1516	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
31	23, 30	sylibr 134	. . . 4 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32		ax-setind 4629	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
33	31, 32	syl 14	. . 3 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34		eleq1 2292	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
35	34	spcgv 2890	. . 3 ⊢ (𝐴 ∈ 𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
36	33, 35	mpd 13	. 2 ⊢ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))
37		neldifsnd 3799	. 2 ⊢ (𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
38	36, 37	pm2.65i 642	1 ⊢ ¬ 𝐴 ∈ 𝐴

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1002  ∀wal 1393   = wceq 1395  [wsb 1808   ∈ wcel 2200  ∀wral 2508  Vcvv 2799   ∖ cdif 3194  {csn 3666

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-setind 4629

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-v 2801  df-dif 3199  df-sn 3672

This theorem is referenced by:  ordirr  4634  elirrv  4640  sucprcreg  4641  ordsoexmid  4654  onnmin  4660  ssnel  4661  ordtri2or2exmid  4663  reg3exmidlemwe  4671  nntri2  6648  nntri3  6651  nndceq  6653  nndcel  6654  phpelm  7036  fiunsnnn  7051  onunsnss  7087  snon0  7110