Theorem elirr 4641

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 4637, we could redefine Ord 𝐴 (df-iord 4465) to also require E Fr 𝐴 (df-frind 4431) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4642 (which under that definition would presumably not need ax-setind 4637 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 4642. To encourage ordirr 4642 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 3805	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2		simp1 1023	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝐴)
3		eleq1 2293	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
4		eleq1 2293	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
6	5	spcgv 2892	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑥 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
7	6	pm2.43b 52	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
8	7	3ad2ant2 1045	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
9		eleq2 2294	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴))
10	9	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
11	10	3ad2ant3 1046	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
12	8, 11	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
13	2, 12	mpd 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14	13	3expia 1231	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
15	1, 14	mtod 669	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16		vex 2804	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		eldif 3208	. . . . . . . . . 10 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
18	16, 17	mpbiran 948	. . . . . . . . 9 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19		velsn 3687	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
20	18, 19	xchbinx 688	. . . . . . . 8 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
21	15, 20	sylibr 134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
22	21	ex 115	. . . . . 6 ⊢ (𝐴 ∈ 𝐴 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
23	22	alrimiv 1921	. . . . 5 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24		df-ral 2514	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25		clelsb1 2335	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
26	25	imbi2i 226	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
27	26	albii 1518	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
28	24, 27	bitri 184	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
29	28	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
30	29	albii 1518	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
31	23, 30	sylibr 134	. . . 4 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32		ax-setind 4637	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
33	31, 32	syl 14	. . 3 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34		eleq1 2293	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
35	34	spcgv 2892	. . 3 ⊢ (𝐴 ∈ 𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
36	33, 35	mpd 13	. 2 ⊢ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))
37		neldifsnd 3805	. 2 ⊢ (𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
38	36, 37	pm2.65i 644	1 ⊢ ¬ 𝐴 ∈ 𝐴

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1004  ∀wal 1395   = wceq 1397  [wsb 1809   ∈ wcel 2201  ∀wral 2509  Vcvv 2801   ∖ cdif 3196  {csn 3670

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-setind 4637

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-v 2803  df-dif 3201  df-sn 3676

This theorem is referenced by:  ordirr  4642  elirrv  4648  sucprcreg  4649  ordsoexmid  4662  onnmin  4668  ssnel  4669  ordtri2or2exmid  4671  reg3exmidlemwe  4679  nntri2  6667  nntri3  6670  nndceq  6672  nndcel  6673  phpelm  7058  fiunsnnn  7075  onunsnss  7114  snon0  7139