Metamath Proof Explorer

Theorem 1wlkdlem4

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

Ref Expression
Hypotheses 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
Assertion 1wlkdlem4 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 1wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3 1wlkd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 1wlkd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5 1wlkd.l ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
6 1wlkd.j ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
7 2 fveq1i ⊢ ( 𝐹 ‘ 0 ) = ( ⟨“ 𝐽 ”⟩ ‘ 0 )
8 1 2 3 4 5 6 1wlkdlem2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )
9 8 elfvexd ⊢ ( 𝜑 → 𝐽 ∈ V )
10 s1fv ⊢ ( 𝐽 ∈ V → ( ⟨“ 𝐽 ”⟩ ‘ 0 ) = 𝐽 )
11 9 10 syl ⊢ ( 𝜑 → ( ⟨“ 𝐽 ”⟩ ‘ 0 ) = 𝐽 )
12 7 11 syl5eq ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝐽 )
13 12 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝐼 ‘ 𝐽 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝐼 ‘ 𝐽 ) )
15 14 5 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑋 } )
16 df-ne ⊢ ( 𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌 )
17 16 6 sylan2br ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
18 13 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑌 ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝐼 ‘ 𝐽 ) )
19 17 18 sseqtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) )
20 15 19 ifpimpda ⊢ ( 𝜑 → if- ( 𝑋 = 𝑌 , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑋 } , { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
21 1 fveq1i ⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 )
22 s2fv0 ⊢ ( 𝑋 ∈ 𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
23 3 22 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 0 ) = 𝑋 )
24 21 23 syl5eq ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝑋 )
25 1 fveq1i ⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 )
26 s2fv1 ⊢ ( 𝑌 ∈ 𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
27 4 26 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 ”⟩ ‘ 1 ) = 𝑌 )
28 25 27 syl5eq ⊢ ( 𝜑 → ( 𝑃 ‘ 1 ) = 𝑌 )
29 eqeq12 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ↔ 𝑋 = 𝑌 ) )
30 sneq ⊢ ( ( 𝑃 ‘ 0 ) = 𝑋 → { ( 𝑃 ‘ 0 ) } = { 𝑋 } )
31 30 adantr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → { ( 𝑃 ‘ 0 ) } = { 𝑋 } )
32 31 eqeq2d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑋 } ) )
33 preq12 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝑋 , 𝑌 } )
34 33 sseq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ↔ { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
35 29 32 34 ifpbi123d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝑋 ∧ ( 𝑃 ‘ 1 ) = 𝑌 ) → ( if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ↔ if- ( 𝑋 = 𝑌 , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑋 } , { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
36 24 28 35 syl2anc ⊢ ( 𝜑 → ( if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ↔ if- ( 𝑋 = 𝑌 , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑋 } , { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
37 20 36 mpbird ⊢ ( 𝜑 → if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
38 c0ex ⊢ 0 ∈ V
39 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 + 1 ) = ( 0 + 1 ) )
40 0p1e1 ⊢ ( 0 + 1 ) = 1
41 39 40 eqtrdi ⊢ ( 𝑘 = 0 → ( 𝑘 + 1 ) = 1 )
42 wkslem2 ⊢ ( ( 𝑘 = 0 ∧ ( 𝑘 + 1 ) = 1 ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
43 41 42 mpdan ⊢ ( 𝑘 = 0 → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
44 38 43 ralsn ⊢ ( ∀ 𝑘 ∈ { 0 } if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
45 37 44 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 0 } if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
46 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 ”⟩ )
47 s1len ⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
48 46 47 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 1
49 48 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 1 )
50 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
51 49 50 eqtri ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 }
52 51 a1i ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 } )
53 52 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ { 0 } if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
54 45 53 mpbird ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )