Theorem wefrc 5657

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 5649	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ( E We 𝐴 → E We 𝐵))
2		n0 4308	. . . 4 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
3		ineq2 4168	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐵 ∩ 𝑥) = (𝐵 ∩ 𝑦))
4	3	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ (𝐵 ∩ 𝑦) = ∅))
5	4	rspcev 3582	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝐵 ∩ 𝑦) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
6	5	ex 417	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
7	6	adantl 486	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
8		inss1 4190	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
9		wefr 5653	. . . . . . . . . . . . 13 ⊢ ( E We 𝐵 → E Fr 𝐵)
10		vex 3459	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
11	10	inex2 5288	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∩ 𝑦) ∈ V
12	11	epfrc 5648	. . . . . . . . . . . . 13 ⊢ (( E Fr 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
13	9, 12	syl3an1 1181	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
14	13	3exp 1137	. . . . . . . . . . 11 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ⊆ 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
15	8, 14	mpi 21	. . . . . . . . . 10 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
16		rexin 4204	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
17	15, 16	imbitrdi 254	. . . . . . . . 9 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
18	17	adantr 485	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
19		elin 3922	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (𝐵 ∩ 𝑥) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥))
20		df-3an 1105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵))
21		3anrot 1117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
22	20, 21	bitr3i 280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
23		wetrep 5656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦))
24	23	expd 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
25	22, 24	sylan2b 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( E We 𝐵 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
26	25	exp44 442	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))))
27	26	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
28	27	com34 92	. . . . . . . . . . . . . . . . . 18 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
29	28	impd 415	. . . . . . . . . . . . . . . . 17 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
30	19, 29	biimtrid 245	. . . . . . . . . . . . . . . 16 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
31	30	imp4a 427	. . . . . . . . . . . . . . 15 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦)))
32	31	com23 87	. . . . . . . . . . . . . 14 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝑧 ∈ (𝐵 ∩ 𝑥) → 𝑧 ∈ 𝑦)))
33	32	ralrimdv 3163	. . . . . . . . . . . . 13 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦))
34		dfss3 3927	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦)
35	33, 34	imbitrrdi 255	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝐵 ∩ 𝑥) ⊆ 𝑦))
36		dfss 3925	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦))
37		in32 4183	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑥) ∩ 𝑦) = ((𝐵 ∩ 𝑦) ∩ 𝑥)
38	37	eqeq2i 2776	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦) ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
39	36, 38	sylbb 222	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
40	39	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
41	40	biimprd 251	. . . . . . . . . . . 12 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))
42	35, 41	syl6 36	. . . . . . . . . . 11 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)))
43	42	expd 420	. . . . . . . . . 10 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))))
44	43	imp4a 427	. . . . . . . . 9 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → (𝐵 ∩ 𝑥) = ∅)))
45	44	reximdvai 3176	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
46	18, 45	syld 48	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
47	7, 46	pm2.61dne 3044	. . . . . 6 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
48	47	ex 417	. . . . 5 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
49	48	exlimdv 1963	. . . 4 ⊢ ( E We 𝐵 → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
50	2, 49	biimtrid 245	. . 3 ⊢ ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
51	1, 50	syl6com 38	. 2 ⊢ ( E We 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)))
52	51	3imp 1128	1 ⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287   E cep 5562   Fr wfr 5613   We wwe 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618

This theorem is referenced by:  tz7.5  6383  onnseq  8332  finminlem  36810