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 ∈ S a < 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 ∈ S a < 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 ∈ S a < b ∧ b < c ∧ F ⁡ a < F ⁡ b ∧ F ⁡ c < F ⁡ b ∨ F ⁡ b < F ⁡ a ∧ F ⁡ b < F ⁡ c