Theorem elirr 4593

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 4589, we could redefine Ord 𝐴 (df-iord 4417) to also require E Fr 𝐴 (df-frind 4383) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4594 (which under that definition would presumably not need ax-setind 4589 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 4594. To encourage ordirr 4594 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 3766	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2		simp1 1000	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝐴)
3		eleq1 2269	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
4		eleq1 2269	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
6	5	spcgv 2861	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑥 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
7	6	pm2.43b 52	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
8	7	3ad2ant2 1022	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
9		eleq2 2270	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴))
10	9	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
11	10	3ad2ant3 1023	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
12	8, 11	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
13	2, 12	mpd 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14	13	3expia 1208	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
15	1, 14	mtod 665	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16		vex 2776	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		eldif 3176	. . . . . . . . . 10 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
18	16, 17	mpbiran 943	. . . . . . . . 9 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19		velsn 3651	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
20	18, 19	xchbinx 684	. . . . . . . 8 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
21	15, 20	sylibr 134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
22	21	ex 115	. . . . . 6 ⊢ (𝐴 ∈ 𝐴 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
23	22	alrimiv 1898	. . . . 5 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24		df-ral 2490	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25		clelsb1 2311	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
26	25	imbi2i 226	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
27	26	albii 1494	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
28	24, 27	bitri 184	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
29	28	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
30	29	albii 1494	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
31	23, 30	sylibr 134	. . . 4 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32		ax-setind 4589	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
33	31, 32	syl 14	. . 3 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34		eleq1 2269	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
35	34	spcgv 2861	. . 3 ⊢ (𝐴 ∈ 𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
36	33, 35	mpd 13	. 2 ⊢ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))
37		neldifsnd 3766	. 2 ⊢ (𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
38	36, 37	pm2.65i 640	1 ⊢ ¬ 𝐴 ∈ 𝐴

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 981  ∀wal 1371   = wceq 1373  [wsb 1786   ∈ wcel 2177  ∀wral 2485  Vcvv 2773   ∖ cdif 3164  {csn 3634

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-setind 4589

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-v 2775  df-dif 3169  df-sn 3640

This theorem is referenced by:  ordirr  4594  elirrv  4600  sucprcreg  4601  ordsoexmid  4614  onnmin  4620  ssnel  4621  ordtri2or2exmid  4623  reg3exmidlemwe  4631  nntri2  6587  nntri3  6590  nndceq  6592  nndcel  6593  phpelm  6970  fiunsnnn  6985  onunsnss  7021  snon0  7044