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

Metamath Proof Explorer

Theorem bnj1177

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 bnj1177.2 ⊢ ( 𝜓 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑋 ) )
bnj1177.3 ⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
bnj1177.9 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 FrSe 𝐴 )
bnj1177.13 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ⊆ 𝐴 )
bnj1177.17 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐴 )
Assertion bnj1177 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) )

Proof

Step Hyp Ref Expression
1 bnj1177.2 ⊢ ( 𝜓 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑋 ) )
2 bnj1177.3 ⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
3 bnj1177.9 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 FrSe 𝐴 )
4 bnj1177.13 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ⊆ 𝐴 )
5 bnj1177.17 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐴 )
6 df-bnj15 ⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )
7 6 simplbi ⊢ ( 𝑅 FrSe 𝐴 → 𝑅 Fr 𝐴 )
8 3 7 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 Fr 𝐴 )
9 bnj1147 ⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
10 ssinss1 ⊢ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴 → ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ⊆ 𝐴 )
11 9 10 ax-mp ⊢ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ⊆ 𝐴
12 2 11 eqsstri ⊢ 𝐶 ⊆ 𝐴
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ⊆ 𝐴 )
14 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
15 3 5 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
16 15 ssrind ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ⊆ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) )
17 1 simp2bi ⊢ ( 𝜓 → 𝑦 ∈ 𝐵 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 )
19 4 18 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐴 )
20 1 simp3bi ⊢ ( 𝜓 → 𝑦 𝑅 𝑋 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 𝑅 𝑋 )
22 bnj1152 ⊢ ( 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑋 ) )
23 19 21 22 sylanbrc ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) )
24 23 18 elind ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) )
25 16 24 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) )
26 25 ne0d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ≠ ∅ )
27 2 neeq1i ⊢ ( 𝐶 ≠ ∅ ↔ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ≠ ∅ )
28 26 27 sylibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≠ ∅ )
29 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
30 3 5 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
31 inex1g ⊢ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V → ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ∈ V )
32 2 31 eqeltrid ⊢ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V → 𝐶 ∈ V )
33 30 32 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ V )
34 8 13 28 33 bnj951 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) )