Theorem zfregs 4657

Description: The strong form of the Axiom of Regularity, which does not require that A be a set. Axiom 6' of [TakeutiZaring] p. 21. The proof makes use of a special case of Proposition 9.4 of [TakeutiZaring] p. 75.

Assertion

Ref	Expression
zfregs	⊢ (A ≠ ∅ → ∃x ∈ A (x ∩ A) = ∅)

Distinct variable group:   x,A

Proof of Theorem zfregs

Step	Hyp	Ref	Expression
1		ne0 2292	. 2 ⊢ (A ≠ ∅ ↔ ∃z z ∈ A)
2		snex 2756	. . . . 5 ⊢ {z} ∈ V
3	2	tz9.1 4656	. . . 4 ⊢ ∃y({z} ⊆ y ⋀ Tr y ⋀ ∀w(({z} ⊆ w ⋀ Tr w) → y ⊆ w))
4		trel 2692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Tr y → ((w ∈ x ⋀ x ∈ y) → w ∈ y))
5		inass 2226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((y ∩ A) ∩ x) = (y ∩ (A ∩ x))
6		incom 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (A ∩ x) = (x ∩ A)
7	6	ineq2i 2217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (y ∩ (A ∩ x)) = (y ∩ (x ∩ A))
8	5, 7	eqtr 1498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((y ∩ A) ∩ x) = (y ∩ (x ∩ A))
9	8	eleq2i 1541	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w ∈ ((y ∩ A) ∩ x) ↔ w ∈ (y ∩ (x ∩ A)))
10		elin 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w ∈ (y ∩ (x ∩ A)) ↔ (w ∈ y ⋀ w ∈ (x ∩ A)))
11	9, 10	bitr2 174	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((w ∈ y ⋀ w ∈ (x ∩ A)) ↔ w ∈ ((y ∩ A) ∩ x))
12		ne0i 2289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w ∈ ((y ∩ A) ∩ x) → ((y ∩ A) ∩ x) ≠ ∅)
13	11, 12	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((w ∈ y ⋀ w ∈ (x ∩ A)) → ((y ∩ A) ∩ x) ≠ ∅)
14	13	ex 373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w ∈ y → (w ∈ (x ∩ A) → ((y ∩ A) ∩ x) ≠ ∅))
15	4, 14	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Tr y → ((w ∈ x ⋀ x ∈ y) → (w ∈ (x ∩ A) → ((y ∩ A) ∩ x) ≠ ∅)))
16	15	exp3a 376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Tr y → (w ∈ x → (x ∈ y → (w ∈ (x ∩ A) → ((y ∩ A) ∩ x) ≠ ∅))))
17	16	com34 36	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Tr y → (w ∈ x → (w ∈ (x ∩ A) → (x ∈ y → ((y ∩ A) ∩ x) ≠ ∅))))
18	17	imp3a 361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr y → ((w ∈ x ⋀ w ∈ (x ∩ A)) → (x ∈ y → ((y ∩ A) ∩ x) ≠ ∅)))
19		inss1 2233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x ∩ A) ⊆ x
20	19	sseli 2068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (w ∈ (x ∩ A) → w ∈ x)
21	20	ancri 297	. . . . . . . . . . . . . . . . . . . 20 ⊢ (w ∈ (x ∩ A) → (w ∈ x ⋀ w ∈ (x ∩ A)))
22	18, 21	syl5 21	. . . . . . . . . . . . . . . . . . 19 ⊢ (Tr y → (w ∈ (x ∩ A) → (x ∈ y → ((y ∩ A) ∩ x) ≠ ∅)))
23	22	19.23adv 1216	. . . . . . . . . . . . . . . . . 18 ⊢ (Tr y → (∃w w ∈ (x ∩ A) → (x ∈ y → ((y ∩ A) ∩ x) ≠ ∅)))
24		ne0 2292	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∩ A) ≠ ∅ ↔ ∃w w ∈ (x ∩ A))
25	23, 24	syl5ib 206	. . . . . . . . . . . . . . . . 17 ⊢ (Tr y → ((x ∩ A) ≠ ∅ → (x ∈ y → ((y ∩ A) ∩ x) ≠ ∅)))
26	25	com23 32	. . . . . . . . . . . . . . . 16 ⊢ (Tr y → (x ∈ y → ((x ∩ A) ≠ ∅ → ((y ∩ A) ∩ x) ≠ ∅)))
27	26	imp 350	. . . . . . . . . . . . . . 15 ⊢ ((Tr y ⋀ x ∈ y) → ((x ∩ A) ≠ ∅ → ((y ∩ A) ∩ x) ≠ ∅))
28	27	necon4d 1631	. . . . . . . . . . . . . 14 ⊢ ((Tr y ⋀ x ∈ y) → (((y ∩ A) ∩ x) = ∅ → (x ∩ A) = ∅))
29	28	anim2d 563	. . . . . . . . . . . . 13 ⊢ ((Tr y ⋀ x ∈ y) → ((x ∈ A ⋀ ((y ∩ A) ∩ x) = ∅) → (x ∈ A ⋀ (x ∩ A) = ∅)))
30	29	expimpd 375	. . . . . . . . . . . 12 ⊢ (Tr y → ((x ∈ y ⋀ (x ∈ A ⋀ ((y ∩ A) ∩ x) = ∅)) → (x ∈ A ⋀ (x ∩ A) = ∅)))
31		elin 2210	. . . . . . . . . . . . . 14 ⊢ (x ∈ (y ∩ A) ↔ (x ∈ y ⋀ x ∈ A))
32	31	anbi1i 483	. . . . . . . . . . . . 13 ⊢ ((x ∈ (y ∩ A) ⋀ ((y ∩ A) ∩ x) = ∅) ↔ ((x ∈ y ⋀ x ∈ A) ⋀ ((y ∩ A) ∩ x) = ∅))
33		anass 441	. . . . . . . . . . . . 13 ⊢ (((x ∈ y ⋀ x ∈ A) ⋀ ((y ∩ A) ∩ x) = ∅) ↔ (x ∈ y ⋀ (x ∈ A ⋀ ((y ∩ A) ∩ x) = ∅)))
34	32, 33	bitr 173	. . . . . . . . . . . 12 ⊢ ((x ∈ (y ∩ A) ⋀ ((y ∩ A) ∩ x) = ∅) ↔ (x ∈ y ⋀ (x ∈ A ⋀ ((y ∩ A) ∩ x) = ∅)))
35	30, 34	syl5ib 206	. . . . . . . . . . 11 ⊢ (Tr y → ((x ∈ (y ∩ A) ⋀ ((y ∩ A) ∩ x) = ∅) → (x ∈ A ⋀ (x ∩ A) = ∅)))
36	35	r19.22dv2 1739	. . . . . . . . . 10 ⊢ (Tr y → (∃x ∈ (y ∩ A)((y ∩ A) ∩ x) = ∅ → ∃x ∈ A (x ∩ A) = ∅))
37		visset 1816	. . . . . . . . . . . 12 ⊢ y ∈ V
38	37	inex1 2721	. . . . . . . . . . 11 ⊢ (y ∩ A) ∈ V
39	38	zfreg2 4606	. . . . . . . . . 10 ⊢ ((y ∩ A) ≠ ∅ → ∃x ∈ (y ∩ A)((y ∩ A) ∩ x) = ∅)
40	36, 39	syl5 21	. . . . . . . . 9 ⊢ (Tr y → ((y ∩ A) ≠ ∅ → ∃x ∈ A (x ∩ A) = ∅))
41		snssi 2470	. . . . . . . . . . . 12 ⊢ (z ∈ A → {z} ⊆ A)
42	41	anim2i 335	. . . . . . . . . . 11 ⊢ (({z} ⊆ y ⋀ z ∈ A) → ({z} ⊆ y ⋀ {z} ⊆ A))
43		ssin 2235	. . . . . . . . . . . 12 ⊢ (({z} ⊆ y ⋀ {z} ⊆ A) ↔ {z} ⊆ (y ∩ A))
44		visset 1816	. . . . . . . . . . . . 13 ⊢ z ∈ V
45	44	snss 2465	. . . . . . . . . . . 12 ⊢ (z ∈ (y ∩ A) ↔ {z} ⊆ (y ∩ A))
46	43, 45	bitr4 176	. . . . . . . . . . 11 ⊢ (({z} ⊆ y ⋀ {z} ⊆ A) ↔ z ∈ (y ∩ A))
47	42, 46	sylib 198	. . . . . . . . . 10 ⊢ (({z} ⊆ y ⋀ z ∈ A) → z ∈ (y ∩ A))
48		ne0i 2289	. . . . . . . . . 10 ⊢ (z ∈ (y ∩ A) → (y ∩ A) ≠ ∅)
49	47, 48	syl 10	. . . . . . . . 9 ⊢ (({z} ⊆ y ⋀ z ∈ A) → (y ∩ A) ≠ ∅)
50	40, 49	syl5 21	. . . . . . . 8 ⊢ (Tr y → (({z} ⊆ y ⋀ z ∈ A) → ∃x ∈ A (x ∩ A) = ∅))
51	50	exp3a 376	. . . . . . 7 ⊢ (Tr y → ({z} ⊆ y → (z ∈ A → ∃x ∈ A (x ∩ A) = ∅)))
52	51	impcom 351	. . . . . 6 ⊢ (({z} ⊆ y ⋀ Tr y) → (z ∈ A → ∃x ∈ A (x ∩ A) = ∅))
53	52	3adant3 801	. . . . 5 ⊢ (({z} ⊆ y ⋀ Tr y ⋀ ∀w(({z} ⊆ w ⋀ Tr w) → y ⊆ w)) → (z ∈ A → ∃x ∈ A (x ∩ A) = ∅))
54	53	19.23aiv 1297	. . . 4 ⊢ (∃y({z} ⊆ y ⋀ Tr y ⋀ ∀w(({z} ⊆ w ⋀ Tr w) → y ⊆ w)) → (z ∈ A → ∃x ∈ A (x ∩ A) = ∅))
55	3, 54	ax-mp 7	. . 3 ⊢ (z ∈ A → ∃x ∈ A (x ∩ A) = ∅)
56	55	19.23aiv 1297	. 2 ⊢ (∃z z ∈ A → ∃x ∈ A (x ∩ A) = ∅)
57	1, 56	sylbi 199	1 ⊢ (A ≠ ∅ → ∃x ∈ A (x ∩ A) = ∅)

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 777  ∀wal 956   = wceq 958   ∈ wcel 960  ∃wex 982   ≠ wne 1588  ∃wrex 1649   ∩ cin 2049   ⊆ wss 2050  ∅c0 2283  {csn 2413  Tr wtr 2685

This theorem is referenced by:  setind 4658

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-reg 4602  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-rab 1655  df-v 1815  df-sbc 1945  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-fv 3204  df-rdg 3938

Copyright terms: Public domain