Metamath Proof Explorer

Theorem bnj1175

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 bnj1175.3 ⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
bnj1175.4 ⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ) )
bnj1175.5 ⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) )
Assertion bnj1175 ( 𝜃 → ( 𝑤 𝑅 𝑧 → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 bnj1175.3 ⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
2 bnj1175.4 ⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ) )
3 bnj1175.5 ⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) )
4 bnj255 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ) )
5 df-bnj17 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑤 𝑅 𝑧 ) )
6 2 4 5 3bitr2i ⊢ ( 𝜒 ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑤 𝑅 𝑧 ) )
7 3 anbi1i ⊢ ( ( 𝜃 ∧ 𝑤 𝑅 𝑧 ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑤 𝑅 𝑧 ) )
8 6 7 bitr4i ⊢ ( 𝜒 ↔ ( 𝜃 ∧ 𝑤 𝑅 𝑧 ) )
9 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
10 2 9 bnj835 ⊢ ( 𝜒 → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
11 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
12 2 11 bnj836 ⊢ ( 𝜒 → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
13 bnj1152 ⊢ ( 𝑤 ∈ pred ( 𝑧 , 𝐴 , 𝑅 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) )
14 13 biimpri ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) → 𝑤 ∈ pred ( 𝑧 , 𝐴 , 𝑅 ) )
15 2 14 bnj837 ⊢ ( 𝜒 → 𝑤 ∈ pred ( 𝑧 , 𝐴 , 𝑅 ) )
16 12 15 sseldd ⊢ ( 𝜒 → 𝑤 ∈ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
17 10 16 sseldd ⊢ ( 𝜒 → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
18 8 17 sylbir ⊢ ( ( 𝜃 ∧ 𝑤 𝑅 𝑧 ) → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
19 18 ex ⊢ ( 𝜃 → ( 𝑤 𝑅 𝑧 → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )