Theorem bnj1173

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1173.3	⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
	bnj1173.5	⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) )
	bnj1173.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 FrSe 𝐴 )
	bnj1173.17	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐴 )
Assertion	bnj1173	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝜃 ↔ 𝑤 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1173.3	⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
2		bnj1173.5	⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) )
3		bnj1173.9	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 FrSe 𝐴 )
4		bnj1173.17	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐴 )
5		3simpc	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) )
6	3	3adant3	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → 𝑅 FrSe 𝐴 )
7	4	3adant3	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 )
8		elin	⊢ ( 𝑧 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ↔ ( 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ 𝐵 ) )
9	8	simplbi	⊢ ( 𝑧 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
10	9 1	eleq2s	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
11	10	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
12		pm3.21	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
13	6 7 11 12	syl3anc	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
14		bnj170	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
15	13 14	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ) )
16	5 15	impbid2	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ) )
17	2 16	bitrid	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ) )
18		bnj1147	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
19	18 11	bnj1213	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐴 )
20	6 19	jca	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
21	20	biantrurd	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑤 ∈ 𝐴 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ) )
22	17 21	bitr4d	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝜃 ↔ 𝑤 ∈ 𝐴 ) )