This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) → ( 𝜃 ↔ 𝑤 ∈ 𝐴 ) )