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	biimpi	⊢ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) → { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) )
10	3	simp2d	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
11	3	simp1d	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
12	11	adantr	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → 𝐴 ∈ 𝑉 )
13		prssg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
14	10 12 13	syl2an2r	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) ↔ { 𝐵 , 𝐴 } ⊆ ( 𝐼 ‘ 𝐽 ) ) )
15	9 14	mpbird	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ) )
16	15	simpld	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) → 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) )
17	16	ex	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) → 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ) )
18		simpr	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) )
19	3	simp3d	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
20	19	adantr	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
21		prssg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) ↔ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
22	10 20 21	syl2an2r	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) ↔ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
23	18 22	mpbird	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐾 ) ) )
24	23	simpld	⊢ ( ( 𝜑 ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) )
25	24	ex	⊢ ( 𝜑 → ( { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) → 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) )
26	17 25	anim12d	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) ) )
27	5 26	mpd	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ) )