Theorem frmin 9438

Description: Every (possibly proper) subclass of a class 𝐴 with a well-founded set-like relation 𝑅 has a minimal element. This is a very strong generalization of tz6.26 6235 and tz7.5 6272. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)

Assertion

Ref	Expression
frmin	⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)

Distinct variable groups:   𝑦,𝐵   𝑦,𝑅

Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem frmin

Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frss 5547	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝑅 Fr 𝐴 → 𝑅 Fr 𝐵))
2		sess2 5549	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se 𝐵))
3	1, 2	anim12d 608	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵)))
4		n0 4277	. . . 4 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏 ∈ 𝐵)
5		predeq3 6195	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑏))
6	5	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, 𝐵, 𝑏) = ∅))
7	6	rspcev 3552	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑏) = ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
8	7	ex 412	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
9	8	adantl 481	. . . . . . 7 ⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
10		setlikespec 6217	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → Pred(𝑅, 𝐵, 𝑏) ∈ V)
11		trpredpred 9406	. . . . . . . . . . . . 13 ⊢ (Pred(𝑅, 𝐵, 𝑏) ∈ V → Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏))
12		ssn0 4331	. . . . . . . . . . . . . 14 ⊢ ((Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) ∧ Pred(𝑅, 𝐵, 𝑏) ≠ ∅) → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)
13	12	ex 412	. . . . . . . . . . . . 13 ⊢ (Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
14	11, 13	syl 17	. . . . . . . . . . . 12 ⊢ (Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
15		trpredss 9407	. . . . . . . . . . . 12 ⊢ (Pred(𝑅, 𝐵, 𝑏) ∈ V → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
16	14, 15	jctild 525	. . . . . . . . . . 11 ⊢ (Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
17	10, 16	syl 17	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
18	17	adantr 480	. . . . . . . . 9 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
19		trpredex 9416	. . . . . . . . . . 11 ⊢ TrPred(𝑅, 𝐵, 𝑏) ∈ V
20		sseq1 3942	. . . . . . . . . . . . . 14 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐 ⊆ 𝐵 ↔ TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵))
21		neeq1 3005	. . . . . . . . . . . . . 14 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐 ≠ ∅ ↔ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
22	20, 21	anbi12d 630	. . . . . . . . . . . . 13 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) ↔ (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
23		predeq2 6194	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝑐, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
24	23	eqeq1d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
25	24	rexeqbi1dv 3332	. . . . . . . . . . . . 13 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
26	22, 25	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) ↔ ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)))
27	26	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑅 Fr 𝐵 → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) ↔ (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))))
28		dffr4 6211	. . . . . . . . . . . 12 ⊢ (𝑅 Fr 𝐵 ↔ ∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
29		sp 2178	. . . . . . . . . . . 12 ⊢ (∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
30	28, 29	sylbi 216	. . . . . . . . . . 11 ⊢ (𝑅 Fr 𝐵 → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
31	19, 27, 30	vtocl 3488	. . . . . . . . . 10 ⊢ (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
32	10, 15	syl 17	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
33	32	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
34		trpredtr 9408	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)))
35	34	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏))
36		sspred 6200	. . . . . . . . . . . . . . 15 ⊢ ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
37	33, 35, 36	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
38	37	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
39	38	biimprd 247	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → Pred(𝑅, 𝐵, 𝑦) = ∅))
40	39	reximdva 3202	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅))
41		ssrexv 3984	. . . . . . . . . . 11 ⊢ (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
42	32, 40, 41	sylsyld 61	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
43	31, 42	sylan9r 508	. . . . . . . . 9 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
44	18, 43	syld 47	. . . . . . . 8 ⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
45	44	an31s 650	. . . . . . 7 ⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
46	9, 45	pm2.61dne 3030	. . . . . 6 ⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
47	46	ex 412	. . . . 5 ⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
48	47	exlimdv 1937	. . . 4 ⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑏 𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
49	4, 48	syl5bi 241	. . 3 ⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
50	3, 49	syl6com 37	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)))
51	50	imp32 418	1 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  Vcvv 3422   ⊆ wss 3883  ∅c0 4253   Fr wfr 5532   Se wse 5533  Predcpred 6190  TrPredctrpred 9395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-inf2 9329

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-trpred 9396

This theorem is referenced by:  frind  9439  frr1  9448