Metamath Proof Explorer

Theorem pmltpclem1

Description: Lemma for pmltpc . (Contributed by Mario Carneiro, 1-Jul-2014)

Ref Expression
Hypotheses pmltpclem1.1 ⊢φ→A∈S
pmltpclem1.2 ⊢φ→B∈S
pmltpclem1.3 ⊢φ→C∈S
pmltpclem1.4 ⊢φ→A<B
pmltpclem1.5 ⊢φ→B<C
pmltpclem1.6 ⊢φ→F⁡A<F⁡B∧F⁡C<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡C
Assertion pmltpclem1 ⊢φ→∃a∈S∃b∈S∃c∈Sa<b∧b<c∧F⁡a<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡a∧F⁡b<F⁡c

Proof

Step Hyp Ref Expression
1 pmltpclem1.1 ⊢φ→A∈S
2 pmltpclem1.2 ⊢φ→B∈S
3 pmltpclem1.3 ⊢φ→C∈S
4 pmltpclem1.4 ⊢φ→A<B
5 pmltpclem1.5 ⊢φ→B<C
6 pmltpclem1.6 ⊢φ→F⁡A<F⁡B∧F⁡C<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡C
7 breq1 ⊢a=A→a<b↔A<b
8 fveq2 ⊢a=A→F⁡a=F⁡A
9 8 breq1d ⊢a=A→F⁡a<F⁡b↔F⁡A<F⁡b
10 9 anbi1d ⊢a=A→F⁡a<F⁡b∧F⁡c<F⁡b↔F⁡A<F⁡b∧F⁡c<F⁡b
11 8 breq2d ⊢a=A→F⁡b<F⁡a↔F⁡b<F⁡A
12 11 anbi1d ⊢a=A→F⁡b<F⁡a∧F⁡b<F⁡c↔F⁡b<F⁡A∧F⁡b<F⁡c
13 10 12 orbi12d ⊢a=A→F⁡a<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡a∧F⁡b<F⁡c↔F⁡A<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡A∧F⁡b<F⁡c
14 7 13 3anbi13d ⊢a=A→a<b∧b<c∧F⁡a<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡a∧F⁡b<F⁡c↔A<b∧b<c∧F⁡A<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡A∧F⁡b<F⁡c
15 breq2 ⊢b=B→A<b↔A<B
16 breq1 ⊢b=B→b<c↔B<c
17 fveq2 ⊢b=B→F⁡b=F⁡B
18 17 breq2d ⊢b=B→F⁡A<F⁡b↔F⁡A<F⁡B
19 17 breq2d ⊢b=B→F⁡c<F⁡b↔F⁡c<F⁡B
20 18 19 anbi12d ⊢b=B→F⁡A<F⁡b∧F⁡c<F⁡b↔F⁡A<F⁡B∧F⁡c<F⁡B
21 17 breq1d ⊢b=B→F⁡b<F⁡A↔F⁡B<F⁡A
22 17 breq1d ⊢b=B→F⁡b<F⁡c↔F⁡B<F⁡c
23 21 22 anbi12d ⊢b=B→F⁡b<F⁡A∧F⁡b<F⁡c↔F⁡B<F⁡A∧F⁡B<F⁡c
24 20 23 orbi12d ⊢b=B→F⁡A<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡A∧F⁡b<F⁡c↔F⁡A<F⁡B∧F⁡c<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡c
25 15 16 24 3anbi123d ⊢b=B→A<b∧b<c∧F⁡A<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡A∧F⁡b<F⁡c↔A<B∧B<c∧F⁡A<F⁡B∧F⁡c<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡c
26 breq2 ⊢c=C→B<c↔B<C
27 fveq2 ⊢c=C→F⁡c=F⁡C
28 27 breq1d ⊢c=C→F⁡c<F⁡B↔F⁡C<F⁡B
29 28 anbi2d ⊢c=C→F⁡A<F⁡B∧F⁡c<F⁡B↔F⁡A<F⁡B∧F⁡C<F⁡B
30 27 breq2d ⊢c=C→F⁡B<F⁡c↔F⁡B<F⁡C
31 30 anbi2d ⊢c=C→F⁡B<F⁡A∧F⁡B<F⁡c↔F⁡B<F⁡A∧F⁡B<F⁡C
32 29 31 orbi12d ⊢c=C→F⁡A<F⁡B∧F⁡c<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡c↔F⁡A<F⁡B∧F⁡C<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡C
33 26 32 3anbi23d ⊢c=C→A<B∧B<c∧F⁡A<F⁡B∧F⁡c<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡c↔A<B∧B<C∧F⁡A<F⁡B∧F⁡C<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡C
34 14 25 33 rspc3ev ⊢A∈S∧B∈S∧C∈S∧A<B∧B<C∧F⁡A<F⁡B∧F⁡C<F⁡B∨F⁡B<F⁡A∧F⁡B<F⁡C→∃a∈S∃b∈S∃c∈Sa<b∧b<c∧F⁡a<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡a∧F⁡b<F⁡c
35 1 2 3 4 5 6 34 syl33anc ⊢φ→∃a∈S∃b∈S∃c∈Sa<b∧b<c∧F⁡a<F⁡b∧F⁡c<F⁡b∨F⁡b<F⁡a∧F⁡b<F⁡c