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 B = f | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
frrlem11.2 F = frecs R A G
frrlem11.3 φ g B h B x g u x h v u = v
frrlem11.4 C = F S z z G F Pred R A z
frrlem12.5 φ R Fr A
frrlem12.6 φ z A Pred R A z S
frrlem12.7 φ z A w S Pred R A w S
frrlem13.8 φ z A S V
frrlem13.9 φ z A S A
frrlem14.10 φ A dom F z A dom F Pred R A dom F z =
Assertion frrlem14 φ dom F = A

Proof

Step Hyp Ref Expression
1 frrlem11.1 B = f | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
2 frrlem11.2 F = frecs R A G
3 frrlem11.3 φ g B h B x g u x h v u = v
4 frrlem11.4 C = F S z z G F Pred R A z
5 frrlem12.5 φ R Fr A
6 frrlem12.6 φ z A Pred R A z S
7 frrlem12.7 φ z A w S Pred R A w S
8 frrlem13.8 φ z A S V
9 frrlem13.9 φ z A S A
10 frrlem14.10 φ A dom F z A dom F Pred R A dom F z =
11 1 2 frrlem7 dom F A
12 11 a1i φ dom F A
13 eldifn z A dom F ¬ z dom F
14 13 adantl φ z A dom F ¬ z dom F
15 1 2 3 4 5 6 7 8 9 frrlem13 φ z A dom F Pred R A dom F z = C B
16 elssuni C B C B
17 15 16 syl φ z A dom F Pred R A dom F z = C B
18 1 2 frrlem5 F = B
19 17 18 sseqtrrdi φ z A dom F Pred R A dom F z = C F
20 dmss C F dom C dom F
21 19 20 syl φ z A dom F Pred R A dom F z = dom C dom F
22 ssun2 z dom F S z
23 vsnid z z
24 22 23 sselii z dom F S z
25 4 dmeqi dom C = dom F S z z G F Pred R A z
26 dmun dom F S z z G F Pred R A z = dom F S dom z z G F Pred R A z
27 ovex z G F Pred R A z V
28 27 dmsnop dom z z G F Pred R A z = z
29 28 uneq2i dom F S dom z z G F Pred R A z = dom F S z
30 25 26 29 3eqtri dom C = dom F S z
31 24 30 eleqtrri z dom C
32 31 a1i φ z A dom F Pred R A dom F z = z dom C
33 21 32 sseldd φ z A dom F Pred R A dom F z = z dom F
34 33 expr φ z A dom F Pred R A dom F z = z dom F
35 14 34 mtod φ z A dom F ¬ Pred R A dom F z =
36 35 nrexdv φ ¬ z A dom F Pred R A dom F z =
37 df-ne A dom F ¬ A dom F =
38 37 10 sylan2br φ ¬ A dom F = z A dom F Pred R A dom F z =
39 38 ex φ ¬ A dom F = z A dom F Pred R A dom F z =
40 36 39 mt3d φ A dom F =
41 ssdif0 A dom F A dom F =
42 40 41 sylibr φ A dom F
43 12 42 eqssd φ dom F = A