Metamath Proof Explorer


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 𝐹 = 𝐴 )