Theorem fpr1 8284

Description: Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023.)

Hypothesis

Ref	Expression
fprr.1	⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)

Assertion

Ref	Expression
fpr1	⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴)

Proof of Theorem fpr1

Dummy variables 𝑥 𝑦 𝑧 𝑢 𝑣 𝑎 𝑏 𝑐 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2762	. . . 4 ⊢ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2	1	frrlem1 8267	. . 3 ⊢ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑎 ∣ ∃𝑏(𝑎 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑐 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑐) ⊆ 𝑏) ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝑐𝐺(𝑎 ↾ Pred(𝑅, 𝐴, 𝑐))))}
3		fprr.1	. . 3 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
4	2, 3	fprlem1 8281	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ∧ ℎ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → ((𝑏𝑔𝑢 ∧ 𝑏ℎ𝑣) → 𝑢 = 𝑣))
5	2, 3, 4	frrlem9 8275	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → Fun 𝐹)
6		eqid 2762	. . 3 ⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
7		simp1 1149	. . 3 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝑅 Fr 𝐴)
8		ssidd 3959	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, 𝐴, 𝑧))
9		fprlem2 8282	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑦) ⊆ Pred(𝑅, 𝐴, 𝑧))
10		setlikespec 6312	. . . . 5 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑧) ∈ V)
11	10	ancoms 462	. . . 4 ⊢ ((𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ∈ V)
12	11	3ad2antl3 1201	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ∈ V)
13		predss 6296	. . . 4 ⊢ Pred(𝑅, 𝐴, 𝑧) ⊆ 𝐴
14	13	a1i 11	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝐴)
15		difssd 4090	. . . . 5 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → (𝐴 ∖ dom 𝐹) ⊆ 𝐴)
16		simpr 488	. . . . 5 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → (𝐴 ∖ dom 𝐹) ≠ ∅)
17	15, 16	jca 519	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ((𝐴 ∖ dom 𝐹) ⊆ 𝐴 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅))
18		frpomin2 6328	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ ((𝐴 ∖ dom 𝐹) ⊆ 𝐴 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅)) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)
19	17, 18	syldan 600	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)
20	2, 3, 4, 6, 7, 8, 9, 12, 14, 19	frrlem14 8280	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → dom 𝐹 = 𝐴)
21		df-fn 6524	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
22	5, 20, 21	sylanbrc 592	1 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098   = wceq 1560  ∃wex 1799   ∈ wcel 2142  {cab 2740   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285  {csn 4582  ⟨cop 4588   Po wpo 5553   Fr wfr 5597   Se wse 5598  dom cdm 5647   ↾ cres 5649  Predcpred 6287  Fun wfun 6515   Fn wfn 6516  ‘cfv 6521  (class class class)co 7396  frecscfrecs 8261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-fr 5600  df-se 5601  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-frecs 8262

This theorem is referenced by:  fpr2  8285  fpr3  8286  wfr1  8307  on2recsfn  8637  norecfn  28036  norec2fn  28046