Metamath Proof Explorer

Theorem 1wlkdlem4

Description: Lemma 4 for 1wlkd . (Contributed by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1wlkd.p ⊢ P = ⟨“ XY ”⟩
1wlkd.f ⊢ F = ⟨“ J ”⟩
1wlkd.x ⊢ φ → X ∈ V
1wlkd.y ⊢ φ → Y ∈ V
1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
Assertion 1wlkdlem4 ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ P = ⟨“ XY ”⟩
2 1wlkd.f ⊢ F = ⟨“ J ”⟩
3 1wlkd.x ⊢ φ → X ∈ V
4 1wlkd.y ⊢ φ → Y ∈ V
5 1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
6 1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
7 2 fveq1i ⊢ F ⁡ 0 = ⟨“ J ”⟩ ⁡ 0
8 1 2 3 4 5 6 1wlkdlem2 ⊢ φ → X ∈ I ⁡ J
9 8 elfvexd ⊢ φ → J ∈ V
10 s1fv ⊢ J ∈ V → ⟨“ J ”⟩ ⁡ 0 = J
11 9 10 syl ⊢ φ → ⟨“ J ”⟩ ⁡ 0 = J
12 7 11 eqtrid ⊢ φ → F ⁡ 0 = J
13 12 fveq2d ⊢ φ → I ⁡ F ⁡ 0 = I ⁡ J
14 13 adantr ⊢ φ ∧ X = Y → I ⁡ F ⁡ 0 = I ⁡ J
15 14 5 eqtrd ⊢ φ ∧ X = Y → I ⁡ F ⁡ 0 = X
16 df-ne ⊢ X ≠ Y ↔ ¬ X = Y
17 16 6 sylan2br ⊢ φ ∧ ¬ X = Y → X Y ⊆ I ⁡ J
18 13 adantr ⊢ φ ∧ ¬ X = Y → I ⁡ F ⁡ 0 = I ⁡ J
19 17 18 sseqtrrd ⊢ φ ∧ ¬ X = Y → X Y ⊆ I ⁡ F ⁡ 0
20 15 19 ifpimpda ⊢ φ → if- X = Y I ⁡ F ⁡ 0 = X X Y ⊆ I ⁡ F ⁡ 0
21 1 fveq1i ⊢ P ⁡ 0 = ⟨“ XY ”⟩ ⁡ 0
22 s2fv0 ⊢ X ∈ V → ⟨“ XY ”⟩ ⁡ 0 = X
23 3 22 syl ⊢ φ → ⟨“ XY ”⟩ ⁡ 0 = X
24 21 23 eqtrid ⊢ φ → P ⁡ 0 = X
25 1 fveq1i ⊢ P ⁡ 1 = ⟨“ XY ”⟩ ⁡ 1
26 s2fv1 ⊢ Y ∈ V → ⟨“ XY ”⟩ ⁡ 1 = Y
27 4 26 syl ⊢ φ → ⟨“ XY ”⟩ ⁡ 1 = Y
28 25 27 eqtrid ⊢ φ → P ⁡ 1 = Y
29 eqeq12 ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → P ⁡ 0 = P ⁡ 1 ↔ X = Y
30 sneq ⊢ P ⁡ 0 = X → P ⁡ 0 = X
31 30 adantr ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → P ⁡ 0 = X
32 31 eqeq2d ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → I ⁡ F ⁡ 0 = P ⁡ 0 ↔ I ⁡ F ⁡ 0 = X
33 preq12 ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → P ⁡ 0 P ⁡ 1 = X Y
34 33 sseq1d ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ↔ X Y ⊆ I ⁡ F ⁡ 0
35 29 32 34 ifpbi123d ⊢ P ⁡ 0 = X ∧ P ⁡ 1 = Y → if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ↔ if- X = Y I ⁡ F ⁡ 0 = X X Y ⊆ I ⁡ F ⁡ 0
36 24 28 35 syl2anc ⊢ φ → if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0 ↔ if- X = Y I ⁡ F ⁡ 0 = X X Y ⊆ I ⁡ F ⁡ 0
37 20 36 mpbird ⊢ φ → if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
38 c0ex ⊢ 0 ∈ V
39 oveq1 ⊢ k = 0 → k + 1 = 0 + 1
40 0p1e1 ⊢ 0 + 1 = 1
41 39 40 eqtrdi ⊢ k = 0 → k + 1 = 1
42 wkslem2 ⊢ k = 0 ∧ k + 1 = 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
43 41 42 mpdan ⊢ k = 0 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
44 38 43 ralsn ⊢ ∀ k ∈ 0 if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ if- P ⁡ 0 = P ⁡ 1 I ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 0 P ⁡ 1 ⊆ I ⁡ F ⁡ 0
45 37 44 sylibr ⊢ φ → ∀ k ∈ 0 if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
46 2 fveq2i ⊢ F = ⟨“ J ”⟩
47 s1len ⊢ ⟨“ J ”⟩ = 1
48 46 47 eqtri ⊢ F = 1
49 48 oveq2i ⊢ 0 ..^ F = 0 ..^ 1
50 fzo01 ⊢ 0 ..^ 1 = 0
51 49 50 eqtri ⊢ 0 ..^ F = 0
52 51 a1i ⊢ φ → 0 ..^ F = 0
53 45 52 raleqtrrdv ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k