Theorem wefrc 5619

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 5611	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ( E We 𝐴 → E We 𝐵))
2		n0 4288	. . . 4 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
3		ineq2 4150	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐵 ∩ 𝑥) = (𝐵 ∩ 𝑦))
4	3	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ (𝐵 ∩ 𝑦) = ∅))
5	4	rspcev 3567	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝐵 ∩ 𝑦) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
6	5	ex 413	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
7	6	adantl 482	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) = ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
8		inss1 4172	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
9		wefr 5615	. . . . . . . . . . . . 13 ⊢ ( E We 𝐵 → E Fr 𝐵)
10		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
11	10	inex2 5253	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∩ 𝑦) ∈ V
12	11	epfrc 5610	. . . . . . . . . . . . 13 ⊢ (( E Fr 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
13	9, 12	syl3an1 1169	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ (𝐵 ∩ 𝑦) ⊆ 𝐵 ∧ (𝐵 ∩ 𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)
14	13	3exp 1125	. . . . . . . . . . 11 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ⊆ 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
15	8, 14	mpi 20	. . . . . . . . . 10 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
16		rexin 4185	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ (𝐵 ∩ 𝑦)((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
17	15, 16	imbitrdi 252	. . . . . . . . 9 ⊢ ( E We 𝐵 → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
18	17	adantr 481	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅)))
19		elin 3906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (𝐵 ∩ 𝑥) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥))
20		df-3an 1094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵))
21		3anrot 1105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
22	20, 21	bitr3i 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
23		wetrep 5618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦))
24	23	expd 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (( E We 𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
25	22, 24	sylan2b 600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( E We 𝐵 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))
26	25	exp44 438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))))
27	26	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑥 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
28	27	com34 91	. . . . . . . . . . . . . . . . . 18 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝑥 → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦)))))
29	28	impd 411	. . . . . . . . . . . . . . . . 17 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
30	19, 29	biimtrid 243	. . . . . . . . . . . . . . . 16 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → 𝑧 ∈ 𝑦))))
31	30	imp4a 423	. . . . . . . . . . . . . . 15 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝐵 ∩ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → 𝑧 ∈ 𝑦)))
32	31	com23 86	. . . . . . . . . . . . . 14 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝑧 ∈ (𝐵 ∩ 𝑥) → 𝑧 ∈ 𝑦)))
33	32	ralrimdv 3138	. . . . . . . . . . . . 13 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦))
34		dfss3 3911	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵 ∩ 𝑥)𝑧 ∈ 𝑦)
35	33, 34	imbitrrdi 253	. . . . . . . . . . . 12 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (𝐵 ∩ 𝑥) ⊆ 𝑦))
36		dfss 3909	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦))
37		in32 4165	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∩ 𝑥) ∩ 𝑦) = ((𝐵 ∩ 𝑦) ∩ 𝑥)
38	37	eqeq2i 2753	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑥) ∩ 𝑦) ↔ (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
39	36, 38	sylbb 220	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (𝐵 ∩ 𝑥) = ((𝐵 ∩ 𝑦) ∩ 𝑥))
40	39	eqeq1d 2742	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → ((𝐵 ∩ 𝑥) = ∅ ↔ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅))
41	40	biimprd 249	. . . . . . . . . . . 12 ⊢ ((𝐵 ∩ 𝑥) ⊆ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))
42	35, 41	syl6 35	. . . . . . . . . . 11 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦) → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅)))
43	42	expd 416	. . . . . . . . . 10 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝑦 → (((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅ → (𝐵 ∩ 𝑥) = ∅))))
44	43	imp4a 423	. . . . . . . . 9 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → (𝐵 ∩ 𝑥) = ∅)))
45	44	reximdvai 3151	. . . . . . . 8 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ ((𝐵 ∩ 𝑦) ∩ 𝑥) = ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
46	18, 45	syld 47	. . . . . . 7 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝐵 ∩ 𝑦) ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
47	7, 46	pm2.61dne 3021	. . . . . 6 ⊢ (( E We 𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)
48	47	ex 413	. . . . 5 ⊢ ( E We 𝐵 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
49	48	exlimdv 1940	. . . 4 ⊢ ( E We 𝐵 → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
50	2, 49	biimtrid 243	. . 3 ⊢ ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅))
51	1, 50	syl6com 37	. 2 ⊢ ( E We 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)))
52	51	3imp 1116	1 ⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  ∀wral 3054  ∃wrex 3064   ∩ cin 3889   ⊆ wss 3890  ∅c0 4268   E cep 5524   Fr wfr 5575   We wwe 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580

This theorem is referenced by:  tz7.5  6338  onnseq  8281  finminlem  36553