Theorem wefrc 5303

Description: A nonempty (possibly proper) subclass of a class well-ordered by E 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 5296	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ( E We 𝐴 → E We 𝐵))
2		n0 4130	. . . 4 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
3		ineq2 4005	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐵 ∩ 𝑥) = (𝐵 ∩ 𝑦))
4	3	eqeq1d 2806	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ (𝐵 ∩ 𝑦) = ∅))
5	4	rspcev 3500	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝐵 ∩ 𝑦) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
6	5	ex 399	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
7	6	adantl 469	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
8		inss1 4027	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
9		wefr 5299	. . . . . . . . . . . . 13 ⊢ ( E We 𝐵 → E Fr 𝐵)
10		vex 3392	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
11	10	inex2 4993	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∩ 𝑦) ∈ V
12	11	epfrc 5295	. . . . . . . . . . . . 13 ⊢ (( E Fr 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
13	9, 12	syl3an1 1195	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
14	13	3exp 1141	. . . . . . . . . . 11 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ⊆ 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
15	8, 14	mpi 20	. . . . . . . . . 10 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
16		elin 3993	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐵 ∩ 𝑦) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦))
17	16	anbi1i 612	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝐵 ∩ 𝑦) ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
18		anass 456	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
19	17, 18	bitri 266	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐵 ∩ 𝑦) ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
20	19	rexbii2 3225	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
21	15, 20	syl6ib 242	. . . . . . . . 9 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
22	21	adantr 468	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
23		elin 3993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (𝐵 ∩ 𝑥) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥))
24		df-3an 1102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵))
25		3anrot 1115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
26	24, 25	bitr3i 268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
27		wetrep 5302	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦))
28	27	expd 402	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
29	26, 28	sylan2b 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( E We 𝐵 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
30	29	exp44 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))))
31	30	imp 395	. . . . . . . . . . . . . . . . . . 19 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
32	31	com34 91	. . . . . . . . . . . . . . . . . 18 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
33	32	impd 398	. . . . . . . . . . . . . . . . 17 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
34	23, 33	syl5bi 233	. . . . . . . . . . . . . . . 16 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
35	34	imp4a 411	. . . . . . . . . . . . . . 15 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦)))
36	35	com23 86	. . . . . . . . . . . . . 14 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝑧 ∈ (𝐵 ∩ 𝑥) → 𝑧 ∈ 𝑦)))
37	36	ralrimdv 3154	. . . . . . . . . . . . 13 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦))
38		dfss3 3785	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦)
39	37, 38	syl6ibr 243	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝐵 ∩ 𝑥) ⊆ 𝑦))
40		dfss 3782	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦))
41		in32 4020	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑥) ∩ 𝑦) = ((𝐵 ∩ 𝑦) ∩ 𝑥)
42	41	eqeq2i 2816	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦) ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
43	40, 42	sylbb 210	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
44	43	eqeq1d 2806	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
45	44	biimprd 239	. . . . . . . . . . . 12 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))
46	39, 45	syl6 35	. . . . . . . . . . 11 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)))
47	46	expd 402	. . . . . . . . . 10 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))))
48	47	imp4a 411	. . . . . . . . 9 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → (𝐵 ∩ 𝑥) = ∅)))
49	48	reximdvai 3200	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
50	22, 49	syld 47	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
51	7, 50	pm2.61dne 3062	. . . . . 6 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
52	51	ex 399	. . . . 5 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
53	52	exlimdv 2024	. . . 4 ⊢ ( E We 𝐵 → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
54	2, 53	syl5bi 233	. . 3 ⊢ ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
55	1, 54	syl6com 37	. 2 ⊢ ( E We 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)))
56	55	3imp 1130	1 ⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100   = wceq 1637  ∃wex 1859   ∈ wcel 2156   ≠ wne 2976  ∀wral 3094  ∃wrex 3095   ∩ cin 3766   ⊆ wss 3767  ∅c0 4114   E cep 5221   Fr wfr 5265   We wwe 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pr 5094

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4843  df-opab 4905  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-we 5270

This theorem is referenced by:  tz7.5  5955  onnseq  7675  finminlem  32631