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 ⊢ ψ ↔ X ∈ B ∧ y ∈ B ∧ y R X
bnj1177.3 ⊢ C = trCl X A R ∩ B
bnj1177.9 ⊢ φ ∧ ψ → R FrSe A
bnj1177.13 ⊢ φ ∧ ψ → B ⊆ A
bnj1177.17 ⊢ φ ∧ ψ → X ∈ A
Assertion bnj1177 ⊢ φ ∧ ψ → R Fr A ∧ C ⊆ A ∧ C ≠ ∅ ∧ C ∈ V

Proof

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