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 = y V w x | w x y
inf3lem.2 F = rec G ω
inf3lem.3 A V
inf3lem.4 B V
Assertion inf3lem5 x x x A ω B A F B F A

Proof

Step Hyp Ref Expression
1 inf3lem.1 G = y V w x | w x y
2 inf3lem.2 F = rec G ω
3 inf3lem.3 A V
4 inf3lem.4 B V
5 elnn B A A ω B ω
6 5 ancoms A ω B A B ω
7 nnord A ω Ord A
8 ordsucss Ord A B A suc B A
9 7 8 syl A ω B A suc B A
10 9 adantr A ω B ω B A suc B A
11 peano2b B ω suc B ω
12 fveq2 v = suc B F v = F suc B
13 12 psseq2d v = suc B F B F v F B F suc B
14 13 imbi2d v = suc B x x x F B F v x x x F B F suc B
15 fveq2 v = u F v = F u
16 15 psseq2d v = u F B F v F B F u
17 16 imbi2d v = u x x x F B F v x x x F B F u
18 fveq2 v = suc u F v = F suc u
19 18 psseq2d v = suc u F B F v F B F suc u
20 19 imbi2d v = suc u x x x F B F v x x x F B F suc u
21 fveq2 v = A F v = F A
22 21 psseq2d v = A F B F v F B F A
23 22 imbi2d v = A x x x F B F v x x x F B F A
24 1 2 4 4 inf3lem4 x x x B ω F B F suc B
25 24 com12 B ω x x x F B F suc B
26 11 25 sylbir suc B ω x x x F B F suc B
27 vex u V
28 1 2 27 4 inf3lem4 x x x u ω F u F suc u
29 psstr F B F u F u F suc u F B F suc u
30 29 expcom F u F suc u F B F u F B F suc u
31 28 30 syl6com u ω x x x F B F u F B F suc u
32 31 a2d u ω x x x F B F u x x x F B F suc u
33 32 ad2antrr u ω suc B ω suc B u x x x F B F u x x x F B F suc u
34 14 17 20 23 26 33 findsg A ω suc B ω suc B A x x x F B F A
35 34 ex A ω suc B ω suc B A x x x F B F A
36 11 35 sylan2b A ω B ω suc B A x x x F B F A
37 10 36 syld A ω B ω B A x x x F B F A
38 37 impancom A ω B A B ω x x x F B F A
39 6 38 mpd A ω B A x x x F B F A
40 39 com12 x x x A ω B A F B F A