Theorem wefrc 2195

Description: A non-empty (possibly proper) subclass of a class well-ordered by E has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31.

Assertion

Ref	Expression
wefrc	⊢ ((E We A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃x ∈ B (B ∩ x) = ∅)

Distinct variable group(s):   x,A   x,B

Proof of Theorem wefrc

Step	Hyp	Ref	Expression
1		wess 2188	. . . 4 ⊢ (B ⊆ A → (E We A → E We B))
2		ineq2 1639	. . . . . . . . . . . 12 ⊢ (x = y → (B ∩ x) = (B ∩ y))
3	2	cleq1d 1109	. . . . . . . . . . 11 ⊢ (x = y → ((B ∩ x) = ∅ ↔ (B ∩ y) = ∅))
4	3	rcla4ev 1403	. . . . . . . . . 10 ⊢ ((y ∈ B ∧ (B ∩ y) = ∅) → ∃x ∈ B (B ∩ x) = ∅)
5	4	exp 291	. . . . . . . . 9 ⊢ (y ∈ B → ((B ∩ y) = ∅ → ∃x ∈ B (B ∩ x) = ∅))
6	5	adantl 305	. . . . . . . 8 ⊢ ((E We B ∧ y ∈ B) → ((B ∩ y) = ∅ → ∃x ∈ B (B ∩ x) = ∅))
7		inss1 1657	. . . . . . . . . . . 12 ⊢ (B ∩ y) ⊆ B
8		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ y ∈ V
9	8	inex2 1698	. . . . . . . . . . . . . . 15 ⊢ (B ∩ y) ∈ V
10	9	epfrc 2185	. . . . . . . . . . . . . 14 ⊢ ((E Fr B ∧ ((B ∩ y) ⊆ B ∧ ¬ (B ∩ y) = ∅)) → ∃x ∈ (B ∩ y)((B ∩ y) ∩ x) = ∅)
11		wefr 2191	. . . . . . . . . . . . . 14 ⊢ (E We B → E Fr B)
12	10, 11	sylan 343	. . . . . . . . . . . . 13 ⊢ ((E We B ∧ ((B ∩ y) ⊆ B ∧ ¬ (B ∩ y) = ∅)) → ∃x ∈ (B ∩ y)((B ∩ y) ∩ x) = ∅)
13	12	exp32 294	. . . . . . . . . . . 12 ⊢ (E We B → ((B ∩ y) ⊆ B → (¬ (B ∩ y) = ∅ → ∃x ∈ (B ∩ y)((B ∩ y) ∩ x) = ∅)))
14	7, 13	mpi 44	. . . . . . . . . . 11 ⊢ (E We B → (¬ (B ∩ y) = ∅ → ∃x ∈ (B ∩ y)((B ∩ y) ∩ x) = ∅))
15		elin 1635	. . . . . . . . . . . . . 14 ⊢ (x ∈ (B ∩ y) ↔ (x ∈ B ∧ x ∈ y))
16	15	anbi1i 368	. . . . . . . . . . . . 13 ⊢ ((x ∈ (B ∩ y) ∧ ((B ∩ y) ∩ x) = ∅) ↔ ((x ∈ B ∧ x ∈ y) ∧ ((B ∩ y) ∩ x) = ∅))
17		anass 336	. . . . . . . . . . . . 13 ⊢ (((x ∈ B ∧ x ∈ y) ∧ ((B ∩ y) ∩ x) = ∅) ↔ (x ∈ B ∧ (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅)))
18	16, 17	bitr 151	. . . . . . . . . . . 12 ⊢ ((x ∈ (B ∩ y) ∧ ((B ∩ y) ∩ x) = ∅) ↔ (x ∈ B ∧ (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅)))
19	18	birex2 1227	. . . . . . . . . . 11 ⊢ (∃x ∈ (B ∩ y)((B ∩ y) ∩ x) = ∅ ↔ ∃x ∈ B (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅))
20	14, 19	syl6ib 185	. . . . . . . . . 10 ⊢ (E We B → (¬ (B ∩ y) = ∅ → ∃x ∈ B (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅)))
21	20	adantr 306	. . . . . . . . 9 ⊢ ((E We B ∧ y ∈ B) → (¬ (B ∩ y) = ∅ → ∃x ∈ B (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅)))
22		wetrep 2194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((E We B ∧ (z ∈ B ∧ x ∈ B ∧ y ∈ B)) → ((z ∈ x ∧ x ∈ y) → z ∈ y))
23	22	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((E We B ∧ (z ∈ B ∧ x ∈ B ∧ y ∈ B)) → (z ∈ x → (x ∈ y → z ∈ y)))
24		df-3an 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y ∈ B ∧ z ∈ B ∧ x ∈ B) ↔ ((y ∈ B ∧ z ∈ B) ∧ x ∈ B))
25		3anrot 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y ∈ B ∧ z ∈ B ∧ x ∈ B) ↔ (z ∈ B ∧ x ∈ B ∧ y ∈ B))
26	24, 25	bitr3 153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y ∈ B ∧ z ∈ B) ∧ x ∈ B) ↔ (z ∈ B ∧ x ∈ B ∧ y ∈ B))
27	23, 26	sylan2b 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((E We B ∧ ((y ∈ B ∧ z ∈ B) ∧ x ∈ B)) → (z ∈ x → (x ∈ y → z ∈ y)))
28	27	exp44 302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (E We B → (y ∈ B → (z ∈ B → (x ∈ B → (z ∈ x → (x ∈ y → z ∈ y))))))
29	28	imp 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((E We B ∧ y ∈ B) → (z ∈ B → (x ∈ B → (z ∈ x → (x ∈ y → z ∈ y)))))
30	29	com34 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((E We B ∧ y ∈ B) → (z ∈ B → (z ∈ x → (x ∈ B → (x ∈ y → z ∈ y)))))
31	30	imp3a 279	. . . . . . . . . . . . . . . . . 18 ⊢ ((E We B ∧ y ∈ B) → ((z ∈ B ∧ z ∈ x) → (x ∈ B → (x ∈ y → z ∈ y))))
32		elin 1635	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ (B ∩ x) ↔ (z ∈ B ∧ z ∈ x))
33	31, 32	syl5ib 181	. . . . . . . . . . . . . . . . 17 ⊢ ((E We B ∧ y ∈ B) → (z ∈ (B ∩ x) → (x ∈ B → (x ∈ y → z ∈ y))))
34	33	imp4a 282	. . . . . . . . . . . . . . . 16 ⊢ ((E We B ∧ y ∈ B) → (z ∈ (B ∩ x) → ((x ∈ B ∧ x ∈ y) → z ∈ y)))
35	34	com23 32	. . . . . . . . . . . . . . 15 ⊢ ((E We B ∧ y ∈ B) → ((x ∈ B ∧ x ∈ y) → (z ∈ (B ∩ x) → z ∈ y)))
36	35	r19.21adv 1262	. . . . . . . . . . . . . 14 ⊢ ((E We B ∧ y ∈ B) → ((x ∈ B ∧ x ∈ y) → ∀z ∈ (B ∩ x)z ∈ y))
37		dfss3 1498	. . . . . . . . . . . . . 14 ⊢ ((B ∩ x) ⊆ y ↔ ∀z ∈ (B ∩ x)z ∈ y)
38	36, 37	syl6ibr 186	. . . . . . . . . . . . 13 ⊢ ((E We B ∧ y ∈ B) → ((x ∈ B ∧ x ∈ y) → (B ∩ x) ⊆ y))
39		dfss 1493	. . . . . . . . . . . . . . . . 17 ⊢ ((B ∩ x) ⊆ y ↔ (B ∩ x) = ((B ∩ x) ∩ y))
40		in23 1652	. . . . . . . . . . . . . . . . . 18 ⊢ ((B ∩ x) ∩ y) = ((B ∩ y) ∩ x)
41	40	cleq2i 1111	. . . . . . . . . . . . . . . . 17 ⊢ ((B ∩ x) = ((B ∩ x) ∩ y) ↔ (B ∩ x) = ((B ∩ y) ∩ x))
42	39, 41	bitr 151	. . . . . . . . . . . . . . . 16 ⊢ ((B ∩ x) ⊆ y ↔ (B ∩ x) = ((B ∩ y) ∩ x))
43	42	biimp 133	. . . . . . . . . . . . . . 15 ⊢ ((B ∩ x) ⊆ y → (B ∩ x) = ((B ∩ y) ∩ x))
44	43	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ ((B ∩ x) ⊆ y → ((B ∩ x) = ∅ ↔ ((B ∩ y) ∩ x) = ∅))
45	44	biimprd 136	. . . . . . . . . . . . 13 ⊢ ((B ∩ x) ⊆ y → (((B ∩ y) ∩ x) = ∅ → (B ∩ x) = ∅))
46	38, 45	syl6 23	. . . . . . . . . . . 12 ⊢ ((E We B ∧ y ∈ B) → ((x ∈ B ∧ x ∈ y) → (((B ∩ y) ∩ x) = ∅ → (B ∩ x) = ∅)))
47	46	exp3a 292	. . . . . . . . . . 11 ⊢ ((E We B ∧ y ∈ B) → (x ∈ B → (x ∈ y → (((B ∩ y) ∩ x) = ∅ → (B ∩ x) = ∅))))
48	47	imp4a 282	. . . . . . . . . 10 ⊢ ((E We B ∧ y ∈ B) → (x ∈ B → ((x ∈ y ∧ ((B ∩ y) ∩ x) = ∅) → (B ∩ x) = ∅)))
49	48	r19.22dv 1278	. . . . . . . . 9 ⊢ ((E We B ∧ y ∈ B) → (∃x ∈ B (x ∈ y ∧ ((B ∩ y) ∩ x) = ∅) → ∃x ∈ B (B ∩ x) = ∅))
50	21, 49	syld 27	. . . . . . . 8 ⊢ ((E We B ∧ y ∈ B) → (¬ (B ∩ y) = ∅ → ∃x ∈ B (B ∩ x) = ∅))
51	6, 50	pm2.61d 112	. . . . . . 7 ⊢ ((E We B ∧ y ∈ B) → ∃x ∈ B (B ∩ x) = ∅)
52	51	exp 291	. . . . . 6 ⊢ (E We B → (y ∈ B → ∃x ∈ B (B ∩ x) = ∅))
53	52	19.23adv 954	. . . . 5 ⊢ (E We B → (∃y y ∈ B → ∃x ∈ B (B ∩ x) = ∅))
54		n0 1714	. . . . 5 ⊢ (¬ B = ∅ ↔ ∃y y ∈ B)
55	53, 54	syl5ib 181	. . . 4 ⊢ (E We B → (¬ B = ∅ → ∃x ∈ B (B ∩ x) = ∅))
56	1, 55	syl6 23	. . 3 ⊢ (B ⊆ A → (E We A → (¬ B = ∅ → ∃x ∈ B (B ∩ x) = ∅)))
57	56	com12 13	. 2 ⊢ (E We A → (B ⊆ A → (¬ B = ∅ → ∃x ∈ B (B ∩ x) = ∅)))
58	57	imp32 281	1 ⊢ ((E We A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃x ∈ B (B ∩ x) = ∅)

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196   ∧ w3a 581  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  Ecep 2056   Fr wfr 2061   We wwe 2062

This theorem is referenced by:  tz7.5 2220

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-eprel 2122  df-po 2128  df-so 2138  df-fr 2169  df-we 2186

metamath.org