HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem acdc3lem 7428
Description: Lemma for acdc3 7429. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (F` x)-. urv, which is unique when r is a well-ordering on A.
Hypotheses
Ref Expression
acdc3lem.1 |- A e. V
acdc3lem.2 |- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
acdc3lem.3 |- G = (S seq1 (NN X. {c}))
Assertion
Ref Expression
acdc3lem |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (G:NN-->A /\ (G` 1) = c /\ A.k e. NN (G` (k + 1)) e. (F` (G` k))))
Distinct variable groups:   u,k,v,x,y,z,A   k,F,u,v,x,y,z   u,G,v,x,y,z   k,c,x,y,z   k,r,u,v,x,y,z
Proof of Theorem acdc3lem
StepHypRef Expression
1 acdc3lem.1 . . . . . 6 |- A e. V
2 acdc3lem.2 . . . . . 6 |- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
31, 1, 2oprabex2 4006 . . . . 5 |- S e. V
4 nnex 5881 . . . . . 6 |- NN e. V
5 snex 2740 . . . . . 6 |- {c} e. V
64, 5xpex 3250 . . . . 5 |- (NN X. {c}) e. V
73, 6seq1f 6260 . . . 4 |- (((NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> (S seq1 (NN X. {c})):NN-->A)
8 snssi 2457 . . . . . 6 |- (c e. A -> {c} (_ A)
9 visset 1804 . . . . . . . 8 |- c e. V
109fconst 3643 . . . . . . 7 |- (NN X. {c}):NN-->{c}
11 fss 3620 . . . . . . 7 |- (((NN X. {c}):NN-->{c} /\ {c} (_ A) -> (NN X. {c}):NN-->A)
1210, 11mpan 693 . . . . . 6 |- ({c} (_ A -> (NN X. {c}):NN-->A)
138, 12syl 10 . . . . 5 |- (c e. A -> (NN X. {c}):NN-->A)
1413ad2antrl 406 . . . 4 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (NN X. {c}):NN-->A)
15 fvex 3717 . . . . . . . . . . . . 13 |- (F` s) e. V
1615rabex 2715 . . . . . . . . . . . 12 |- {v e. (F` s) | A.u e. (F` s) -. urv} e. V
1716uniex 2861 . . . . . . . . . . 11 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} e. V
18 fveq2 3709 . . . . . . . . . . . . 13 |- (x = s -> (F` x) = (F` s))
19 rabeq 1800 . . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` x) -. urv})
20 raleq1 1778 . . . . . . . . . . . . . . 15 |- ((F` x) = (F` s) -> (A.u e. (F` x) -. urv <-> A.u e. (F` s) -. urv))
2120rabbisdv 1798 . . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` s) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
2219, 21eqtrd 1499 . . . . . . . . . . . . 13 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
2318, 22syl 10 . . . . . . . . . . . 12 |- (x = s -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
2423unieqd 2502 . . . . . . . . . . 11 |- (x = s -> U.{v e. (F` x) | A.u e. (F` x) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
25 eqid 1468 . . . . . . . . . . . 12 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv}
2625a1i 8 . . . . . . . . . . 11 |- (y = t -> U.{v e. (F` s) | A.u e. (F` s) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
2717, 24, 26, 2oprabval2 4013 . . . . . . . . . 10 |- ((s e. A /\ t e. A) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
2827adantl 388 . . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
29 ffvelrn 3799 . . . . . . . . . . . . . . 15 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. (P~A \ {(/)}))
30 eldifi 2152 . . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) e. P~A)
3129, 30syl 10 . . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. P~A)
3231adantll 392 . . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) e. P~A)
33 elpwi 2396 . . . . . . . . . . . . 13 |- ((F` s) e. P~A -> (F` s) (_ A)
3432, 33syl 10 . . . . . . . . . . . 12 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) (_ A)
3515wereucl 2936 . . . . . . . . . . . . 13 |- ((r We A /\ (F` s) (_ A /\ (F` s) =/= (/)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
36 simpll 412 . . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> r We A)
37 eldifn 2153 . . . . . . . . . . . . . . . 16 |- ((F` s) e. (P~A \ {(/)}) -> -. (F` s) e. {(/)})
38 id 59 . . . . . . . . . . . . . . . . . 18 |- ((F` s) = (/) -> (F` s) = (/))
39 0ex 2701 . . . . . . . . . . . . . . . . . . 19 |- (/) e. V
4039snid 2425 . . . . . . . . . . . . . . . . . 18 |- (/) e. {(/)}
4138, 40syl6eqel 1548 . . . . . . . . . . . . . . . . 17 |- ((F` s) = (/) -> (F` s) e. {(/)})
4241necon3bi 1599 . . . . . . . . . . . . . . . 16 |- (-. (F` s) e. {(/)} -> (F` s) =/= (/))
4337, 42syl 10 . . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) =/= (/))
4429, 43syl 10 . . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) =/= (/))
4544adantll 392 . . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) =/= (/))
4635, 36, 34, 45syl3anc 856 . . . . . . . . . . . 12 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
4734, 46sseldd 2058 . . . . . . . . . . 11 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
4847adantlrl 398 . . . . . . . . . 10 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
4948adantrr 395 . . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
5028, 49eqeltrd 1540 . . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) e. A)
5150ex 373 . . . . . . 7 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> ((s e. A /\ t e. A) -> (sSt) e. A))
5251r19.21aivv 1712 . . . . . 6 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> A.s e. A A.t e. A (sSt) e. A)
53 fvex 3717 . . . . . . . . 9 |- (F` x) e. V
5453rabex 2715 . . . . . . . 8 |- {v e. (F` x) | A.u e. (F` x) -. urv} e. V
5554uniex 2861 . . . . . . 7 |- U.{v e. (F` x) | A.u e. (F` x) -. urv} e. V
5655, 2fnoprab2 4106 . . . . . 6 |- S Fn (A X. A)
5752, 56jctil 292 . . . . 5 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (