Theorem wefrc 5530

Description: A nonempty subclass of a class well-ordered by membership has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by NM, 17-Feb-2004.)

Assertion

Ref	Expression
wefrc	⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem wefrc

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wess 5523	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ( E We 𝐴 → E We 𝐵))
2		n0 4247	. . . 4 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
3		ineq2 4107	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐵 ∩ 𝑥) = (𝐵 ∩ 𝑦))
4	3	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ (𝐵 ∩ 𝑦) = ∅))
5	4	rspcev 3527	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝐵 ∩ 𝑦) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
6	5	ex 416	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
7	6	adantl 485	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
8		inss1 4129	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
9		wefr 5526	. . . . . . . . . . . . 13 ⊢ ( E We 𝐵 → E Fr 𝐵)
10		vex 3402	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
11	10	inex2 5196	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∩ 𝑦) ∈ V
12	11	epfrc 5522	. . . . . . . . . . . . 13 ⊢ (( E Fr 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
13	9, 12	syl3an1 1165	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
14	13	3exp 1121	. . . . . . . . . . 11 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ⊆ 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
15	8, 14	mpi 20	. . . . . . . . . 10 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
16		rexin 4140	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
17	15, 16	syl6ib 254	. . . . . . . . 9 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
18	17	adantr 484	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
19		elin 3869	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (𝐵 ∩ 𝑥) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥))
20		df-3an 1091	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵))
21		3anrot 1102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
22	20, 21	bitr3i 280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
23		wetrep 5529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦))
24	23	expd 419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
25	22, 24	sylan2b 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( E We 𝐵 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
26	25	exp44 441	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))))
27	26	imp 410	. . . . . . . . . . . . . . . . . . 19 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
28	27	com34 91	. . . . . . . . . . . . . . . . . 18 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
29	28	impd 414	. . . . . . . . . . . . . . . . 17 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
30	19, 29	syl5bi 245	. . . . . . . . . . . . . . . 16 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
31	30	imp4a 426	. . . . . . . . . . . . . . 15 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦)))
32	31	com23 86	. . . . . . . . . . . . . 14 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝑧 ∈ (𝐵 ∩ 𝑥) → 𝑧 ∈ 𝑦)))
33	32	ralrimdv 3099	. . . . . . . . . . . . 13 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦))
34		dfss3 3875	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦)
35	33, 34	syl6ibr 255	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝐵 ∩ 𝑥) ⊆ 𝑦))
36		dfss 3871	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦))
37		in32 4122	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑥) ∩ 𝑦) = ((𝐵 ∩ 𝑦) ∩ 𝑥)
38	37	eqeq2i 2749	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦) ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
39	36, 38	sylbb 222	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
40	39	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
41	40	biimprd 251	. . . . . . . . . . . 12 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))
42	35, 41	syl6 35	. . . . . . . . . . 11 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)))
43	42	expd 419	. . . . . . . . . 10 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))))
44	43	imp4a 426	. . . . . . . . 9 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → (𝐵 ∩ 𝑥) = ∅)))
45	44	reximdvai 3181	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
46	18, 45	syld 47	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
47	7, 46	pm2.61dne 3018	. . . . . 6 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
48	47	ex 416	. . . . 5 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
49	48	exlimdv 1941	. . . 4 ⊢ ( E We 𝐵 → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
50	2, 49	syl5bi 245	. . 3 ⊢ ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
51	1, 50	syl6com 37	. 2 ⊢ ( E We 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)))
52	51	3imp 1113	1 ⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  ∃wrex 3052   ∩ cin 3852   ⊆ wss 3853  ∅c0 4223   E cep 5444   Fr wfr 5491   We wwe 5493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496

This theorem is referenced by:  tz7.5  6212  onnseq  8059  finminlem  34193