Theorem frrlem14

Description: Lemma for well-founded recursion. Finally, we tie all these threads together and show that dom F = A when given the right S . Specifically, we prove that there can be no R -minimal element of ( A \ dom F ) . (Contributed by Scott Fenton, 7-Dec-2022)

	Ref	Expression
Hypotheses	frrlem11.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	frrlem11.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
	frrlem11.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
	frrlem11.4	⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
	frrlem12.5	⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
	frrlem12.6	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
	frrlem12.7	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
	frrlem13.8	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ∈ V )
	frrlem13.9	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ⊆ 𝐴 )
	frrlem14.10	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
Assertion	frrlem14	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		frrlem11.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		frrlem11.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3		frrlem11.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
4		frrlem11.4	⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5		frrlem12.5	⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
6		frrlem12.6	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
7		frrlem12.7	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
8		frrlem13.8	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ∈ V )
9		frrlem13.9	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ⊆ 𝐴 )
10		frrlem14.10	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
11	1 2	frrlem7	⊢ dom 𝐹 ⊆ 𝐴
12	11	a1i	⊢ ( 𝜑 → dom 𝐹 ⊆ 𝐴 )
13		eldifn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ 𝑧 ∈ dom 𝐹 )
15	1 2 3 4 5 6 7 8 9	frrlem13	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ∈ 𝐵 )
16		elssuni	⊢ ( 𝐶 ∈ 𝐵 → 𝐶 ⊆ ∪ 𝐵 )
17	15 16	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ⊆ ∪ 𝐵 )
18	1 2	frrlem5	⊢ 𝐹 = ∪ 𝐵
19	17 18	sseqtrrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ⊆ 𝐹 )
20		dmss	⊢ ( 𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹 )
21	19 20	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → dom 𝐶 ⊆ dom 𝐹 )
22		ssun2	⊢ { 𝑧 } ⊆ ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } )
23		vsnid	⊢ 𝑧 ∈ { 𝑧 }
24	22 23	sselii	⊢ 𝑧 ∈ ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } )
25	4	dmeqi	⊢ dom 𝐶 = dom ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
26		dmun	⊢ dom ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom ( 𝐹 ↾ 𝑆 ) ∪ dom { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
27		ovex	⊢ ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
28	27	dmsnop	⊢ dom { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } = { 𝑧 }
29	28	uneq2i	⊢ ( dom ( 𝐹 ↾ 𝑆 ) ∪ dom { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } )
30	25 26 29	3eqtri	⊢ dom 𝐶 = ( dom ( 𝐹 ↾ 𝑆 ) ∪ { 𝑧 } )
31	24 30	eleqtrri	⊢ 𝑧 ∈ dom 𝐶
32	31	a1i	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑧 ∈ dom 𝐶 )
33	21 32	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑧 ∈ dom 𝐹 )
34	33	expr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ → 𝑧 ∈ dom 𝐹 ) )
35	14 34	mtod	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ¬ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
36	35	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
37		df-ne	⊢ ( ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ )
38	37 10	sylan2br	⊢ ( ( 𝜑 ∧ ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
39	38	ex	⊢ ( 𝜑 → ( ¬ ( 𝐴 ∖ dom 𝐹 ) = ∅ → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) )
40	36 39	mt3d	⊢ ( 𝜑 → ( 𝐴 ∖ dom 𝐹 ) = ∅ )
41		ssdif0	⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ( 𝐴 ∖ dom 𝐹 ) = ∅ )
42	40 41	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
43	12 42	eqssd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )