Metamath Proof Explorer


Theorem inf3lem5

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 G=yVwx|wxy
inf3lem.2 F=recGω
inf3lem.3 AV
inf3lem.4 BV
Assertion inf3lem5 xxxAωBAFBFA

Proof

Step Hyp Ref Expression
1 inf3lem.1 G=yVwx|wxy
2 inf3lem.2 F=recGω
3 inf3lem.3 AV
4 inf3lem.4 BV
5 elnn BAAωBω
6 5 ancoms AωBABω
7 nnord AωOrdA
8 ordsucss OrdABAsucBA
9 7 8 syl AωBAsucBA
10 9 adantr AωBωBAsucBA
11 peano2b BωsucBω
12 fveq2 v=sucBFv=FsucB
13 12 psseq2d v=sucBFBFvFBFsucB
14 13 imbi2d v=sucBxxxFBFvxxxFBFsucB
15 fveq2 v=uFv=Fu
16 15 psseq2d v=uFBFvFBFu
17 16 imbi2d v=uxxxFBFvxxxFBFu
18 fveq2 v=sucuFv=Fsucu
19 18 psseq2d v=sucuFBFvFBFsucu
20 19 imbi2d v=sucuxxxFBFvxxxFBFsucu
21 fveq2 v=AFv=FA
22 21 psseq2d v=AFBFvFBFA
23 22 imbi2d v=AxxxFBFvxxxFBFA
24 1 2 4 4 inf3lem4 xxxBωFBFsucB
25 24 com12 BωxxxFBFsucB
26 11 25 sylbir sucBωxxxFBFsucB
27 vex uV
28 1 2 27 4 inf3lem4 xxxuωFuFsucu
29 psstr FBFuFuFsucuFBFsucu
30 29 expcom FuFsucuFBFuFBFsucu
31 28 30 syl6com uωxxxFBFuFBFsucu
32 31 a2d uωxxxFBFuxxxFBFsucu
33 32 ad2antrr uωsucBωsucBuxxxFBFuxxxFBFsucu
34 14 17 20 23 26 33 findsg AωsucBωsucBAxxxFBFA
35 34 ex AωsucBωsucBAxxxFBFA
36 11 35 sylan2b AωBωsucBAxxxFBFA
37 10 36 syld AωBωBAxxxFBFA
38 37 impancom AωBABωxxxFBFA
39 6 38 mpd AωBAxxxFBFA
40 39 com12 xxxAωBAFBFA