Metamath Proof Explorer

Theorem 3wlkdlem6

Description: Lemma 6 for 3wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
Assertion 3wlkdlem6 ⊢ φ → A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
2 3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3 3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
4 3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
5 3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
6 1 2 3 3wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D
7 preq12 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 P ⁡ 1 = A B
8 7 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ↔ A B ⊆ I ⁡ J
9 8 adantr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ↔ A B ⊆ I ⁡ J
10 preq12 ⊢ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 P ⁡ 2 = B C
11 10 ad2ant2lr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 P ⁡ 2 = B C
12 11 sseq1d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K ↔ B C ⊆ I ⁡ K
13 preq12 ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 = C D
14 13 sseq1d ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L ↔ C D ⊆ I ⁡ L
15 14 adantl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L ↔ C D ⊆ I ⁡ L
16 9 12 15 3anbi123d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L ↔ A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
17 5 16 syl5ibrcom ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L
18 6 17 mpd ⊢ φ → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L
19 fvex ⊢ P ⁡ 0 ∈ V
20 fvex ⊢ P ⁡ 1 ∈ V
21 19 20 prss ⊢ P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ J ↔ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J
22 simpl ⊢ P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ J → P ⁡ 0 ∈ I ⁡ J
23 21 22 sylbir ⊢ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J → P ⁡ 0 ∈ I ⁡ J
24 fvex ⊢ P ⁡ 2 ∈ V
25 20 24 prss ⊢ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ K ↔ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K
26 simpl ⊢ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ K → P ⁡ 1 ∈ I ⁡ K
27 25 26 sylbir ⊢ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K → P ⁡ 1 ∈ I ⁡ K
28 fvex ⊢ P ⁡ 3 ∈ V
29 24 28 prss ⊢ P ⁡ 2 ∈ I ⁡ L ∧ P ⁡ 3 ∈ I ⁡ L ↔ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L
30 simpl ⊢ P ⁡ 2 ∈ I ⁡ L ∧ P ⁡ 3 ∈ I ⁡ L → P ⁡ 2 ∈ I ⁡ L
31 29 30 sylbir ⊢ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L → P ⁡ 2 ∈ I ⁡ L
32 23 27 31 3anim123i ⊢ P ⁡ 0 P ⁡ 1 ⊆ I ⁡ J ∧ P ⁡ 1 P ⁡ 2 ⊆ I ⁡ K ∧ P ⁡ 2 P ⁡ 3 ⊆ I ⁡ L → P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ L
33 18 32 syl ⊢ φ → P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ L
34 eleq1 ⊢ P ⁡ 0 = A → P ⁡ 0 ∈ I ⁡ J ↔ A ∈ I ⁡ J
35 34 adantr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 0 ∈ I ⁡ J ↔ A ∈ I ⁡ J
36 35 adantr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 ∈ I ⁡ J ↔ A ∈ I ⁡ J
37 eleq1 ⊢ P ⁡ 1 = B → P ⁡ 1 ∈ I ⁡ K ↔ B ∈ I ⁡ K
38 37 adantl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B → P ⁡ 1 ∈ I ⁡ K ↔ B ∈ I ⁡ K
39 38 adantr ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 1 ∈ I ⁡ K ↔ B ∈ I ⁡ K
40 eleq1 ⊢ P ⁡ 2 = C → P ⁡ 2 ∈ I ⁡ L ↔ C ∈ I ⁡ L
41 40 adantr ⊢ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 ∈ I ⁡ L ↔ C ∈ I ⁡ L
42 41 adantl ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 2 ∈ I ⁡ L ↔ C ∈ I ⁡ L
43 36 39 42 3anbi123d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ L ↔ A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L
44 43 bicomd ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D → A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L ↔ P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ L
45 6 44 syl ⊢ φ → A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L ↔ P ⁡ 0 ∈ I ⁡ J ∧ P ⁡ 1 ∈ I ⁡ K ∧ P ⁡ 2 ∈ I ⁡ L
46 33 45 mpbird ⊢ φ → A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L