Metamath Proof Explorer


Theorem wfrlem16

Description: Lemma for well-ordered recursion. If z is R minimal in ( A \ dom F ) , then C is acceptable and thus a subset of F , but dom C is bigger than dom F . Thus, z cannot be minimal, so ( A \ dom F ) must be empty, and (due to wfrdmss ), dom F = A . (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13.1 R We A
wfrlem13.2 R Se A
wfrlem13.3 F = wrecs R A G
wfrlem13.4 C = F z G F Pred R A z
Assertion wfrlem16 dom F = A

Proof

Step Hyp Ref Expression
1 wfrlem13.1 R We A
2 wfrlem13.2 R Se A
3 wfrlem13.3 F = wrecs R A G
4 wfrlem13.4 C = F z G F Pred R A z
5 3 wfrdmss dom F A
6 eldifn z A dom F ¬ z dom F
7 ssun2 z dom F z
8 vsnid z z
9 7 8 sselii z dom F z
10 4 dmeqi dom C = dom F z G F Pred R A z
11 dmun dom F z G F Pred R A z = dom F dom z G F Pred R A z
12 fvex G F Pred R A z V
13 12 dmsnop dom z G F Pred R A z = z
14 13 uneq2i dom F dom z G F Pred R A z = dom F z
15 10 11 14 3eqtri dom C = dom F z
16 9 15 eleqtrri z dom C
17 1 2 3 4 wfrlem15 z A dom F Pred R A dom F z = C f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y
18 elssuni C f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y C f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y
19 17 18 syl z A dom F Pred R A dom F z = C f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y
20 df-wrecs wrecs R A G = f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y
21 3 20 eqtri F = f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y
22 19 21 sseqtrrdi z A dom F Pred R A dom F z = C F
23 dmss C F dom C dom F
24 22 23 syl z A dom F Pred R A dom F z = dom C dom F
25 24 sseld z A dom F Pred R A dom F z = z dom C z dom F
26 16 25 mpi z A dom F Pred R A dom F z = z dom F
27 6 26 mtand z A dom F ¬ Pred R A dom F z =
28 27 nrex ¬ z A dom F Pred R A dom F z =
29 df-ne A dom F ¬ A dom F =
30 difss A dom F A
31 1 2 tz6.26i A dom F A A dom F z A dom F Pred R A dom F z =
32 30 31 mpan A dom F z A dom F Pred R A dom F z =
33 29 32 sylbir ¬ A dom F = z A dom F Pred R A dom F z =
34 28 33 mt3 A dom F =
35 ssdif0 A dom F A dom F =
36 34 35 mpbir A dom F
37 5 36 eqssi dom F = A