Theorem elirr 4610

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 4606, we could redefine Ord 𝐴 (df-iord 4434) to also require E Fr 𝐴 (df-frind 4400) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4611 (which under that definition would presumably not need ax-setind 4606 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 4611. To encourage ordirr 4611 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 3778	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2		simp1 1002	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝐴)
3		eleq1 2272	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
4		eleq1 2272	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
6	5	spcgv 2870	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑥 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
7	6	pm2.43b 52	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
8	7	3ad2ant2 1024	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
9		eleq2 2273	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴))
10	9	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
11	10	3ad2ant3 1025	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
12	8, 11	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
13	2, 12	mpd 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14	13	3expia 1210	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
15	1, 14	mtod 667	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16		vex 2782	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		eldif 3186	. . . . . . . . . 10 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
18	16, 17	mpbiran 945	. . . . . . . . 9 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19		velsn 3663	. . . . . . . . 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 1900	. . . . 5 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24		df-ral 2493	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25		clelsb1 2314	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
26	25	imbi2i 226	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
27	26	albii 1496	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
28	24, 27	bitri 184	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
29	28	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
30	29	albii 1496	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
31	23, 30	sylibr 134	. . . 4 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32		ax-setind 4606	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
33	31, 32	syl 14	. . 3 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34		eleq1 2272	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
35	34	spcgv 2870	. . 3 ⊢ (𝐴 ∈ 𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
36	33, 35	mpd 13	. 2 ⊢ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))
37		neldifsnd 3778	. 2 ⊢ (𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
38	36, 37	pm2.65i 642	1 ⊢ ¬ 𝐴 ∈ 𝐴

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 983  ∀wal 1373   = wceq 1375  [wsb 1788   ∈ wcel 2180  ∀wral 2488  Vcvv 2779   ∖ cdif 3174  {csn 3646

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-setind 4606

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-v 2781  df-dif 3179  df-sn 3652

This theorem is referenced by:  ordirr  4611  elirrv  4617  sucprcreg  4618  ordsoexmid  4631  onnmin  4637  ssnel  4638  ordtri2or2exmid  4640  reg3exmidlemwe  4648  nntri2  6610  nntri3  6613  nndceq  6615  nndcel  6616  phpelm  6996  fiunsnnn  7011  onunsnss  7047  snon0  7070