Theorem 2wlkdlem6

Description: Lemma 6 for 2wlkd . (Contributed by AV, 23-Jan-2021)

	Ref	Expression
Hypotheses	2wlkd.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
	2wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
	2wlkd.s	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
	2wlkd.n	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
	2wlkd.e	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
Assertion	2wlkdlem6	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2		2wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3		2wlkd.s	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4		2wlkd.n	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
5		2wlkd.e	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
6		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
7	6	sseq1i	⊢ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
8	7	bilani	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
9	3	simp2d	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
10	3	simp1d	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
11	10	adantr	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → 𝐴 ∈ 𝑉 )
12		prssg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
13	9 11 12	syl2an2r	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
14	8 13	mpbird	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) )
15	14	simpld	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) )
16	15	ex	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) → 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) )
18	3	simp3d	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
19	18	adantr	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
20		prssg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) ↔ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
21	9 19 20	syl2an2r	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) ↔ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
22	17 21	mpbird	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) )
23	22	simpld	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) )
24	23	ex	⊢ ( 𝜑 → ( { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) → 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) )
25	16 24	anim12d	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) ) )
26	5 25	mpd	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) )