Theorem elirr 4540

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 4536, we could redefine Ord 𝐴 (df-iord 4366) to also require E Fr 𝐴 (df-frind 4332) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4541 (which under that definition would presumably not need ax-setind 4536 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 4541. To encourage ordirr 4541 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 3723	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝐴 ∈ (V ∖ {𝐴}))
2		simp1 997	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝐴)
3		eleq1 2240	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
4		eleq1 2240	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
5	3, 4	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
6	5	spcgv 2824	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑥 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴}))))
7	6	pm2.43b 52	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
8	7	3ad2ant2 1019	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})))
9		eleq2 2241	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴))
10	9	imbi1d 231	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
11	10	3ad2ant3 1020	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → ((𝐴 ∈ 𝑥 → 𝐴 ∈ (V ∖ {𝐴})) ↔ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))))
12	8, 11	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
13	2, 12	mpd 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) ∧ 𝑥 = 𝐴) → 𝐴 ∈ (V ∖ {𝐴}))
14	13	3expia 1205	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → (𝑥 = 𝐴 → 𝐴 ∈ (V ∖ {𝐴})))
15	1, 14	mtod 663	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → ¬ 𝑥 = 𝐴)
16		vex 2740	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
17		eldif 3138	. . . . . . . . . 10 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ {𝐴}))
18	16, 17	mpbiran 940	. . . . . . . . 9 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 ∈ {𝐴})
19		velsn 3609	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
20	18, 19	xchbinx 682	. . . . . . . 8 ⊢ (𝑥 ∈ (V ∖ {𝐴}) ↔ ¬ 𝑥 = 𝐴)
21	15, 20	sylibr 134	. . . . . . 7 ⊢ ((𝐴 ∈ 𝐴 ∧ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴}))) → 𝑥 ∈ (V ∖ {𝐴}))
22	21	ex 115	. . . . . 6 ⊢ (𝐴 ∈ 𝐴 → (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
23	22	alrimiv 1874	. . . . 5 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
24		df-ral 2460	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})))
25		clelsb1 2282	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ 𝑦 ∈ (V ∖ {𝐴}))
26	25	imbi2i 226	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
27	26	albii 1470	. . . . . . . 8 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
28	24, 27	bitri 184	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})))
29	28	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
30	29	albii 1470	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) ↔ ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ (V ∖ {𝐴})) → 𝑥 ∈ (V ∖ {𝐴})))
31	23, 30	sylibr 134	. . . 4 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})))
32		ax-setind 4536	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝑥 ∈ (V ∖ {𝐴}) → 𝑥 ∈ (V ∖ {𝐴})) → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
33	31, 32	syl 14	. . 3 ⊢ (𝐴 ∈ 𝐴 → ∀𝑥 𝑥 ∈ (V ∖ {𝐴}))
34		eleq1 2240	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (V ∖ {𝐴}) ↔ 𝐴 ∈ (V ∖ {𝐴})))
35	34	spcgv 2824	. . 3 ⊢ (𝐴 ∈ 𝐴 → (∀𝑥 𝑥 ∈ (V ∖ {𝐴}) → 𝐴 ∈ (V ∖ {𝐴})))
36	33, 35	mpd 13	. 2 ⊢ (𝐴 ∈ 𝐴 → 𝐴 ∈ (V ∖ {𝐴}))
37		neldifsnd 3723	. 2 ⊢ (𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ (V ∖ {𝐴}))
38	36, 37	pm2.65i 639	1 ⊢ ¬ 𝐴 ∈ 𝐴

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978  ∀wal 1351   = wceq 1353  [wsb 1762   ∈ wcel 2148  ∀wral 2455  Vcvv 2737   ∖ cdif 3126  {csn 3592

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-setind 4536

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-v 2739  df-dif 3131  df-sn 3598

This theorem is referenced by:  ordirr  4541  elirrv  4547  sucprcreg  4548  ordsoexmid  4561  onnmin  4567  ssnel  4568  ordtri2or2exmid  4570  reg3exmidlemwe  4578  nntri2  6494  nntri3  6497  nndceq  6499  nndcel  6500  phpelm  6865  fiunsnnn  6880  onunsnss  6915  snon0  6934