Metamath Proof Explorer

Theorem bnj1413

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1413.1 ⊢ B = pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R
Assertion bnj1413 ⊢ R FrSe A ∧ X ∈ A → B ∈ V

Proof

Step Hyp Ref Expression
1 bnj1413.1 ⊢ B = pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R
2 bnj1148 ⊢ R FrSe A ∧ X ∈ A → pred X A R ∈ V
3 bnj893 ⊢ R FrSe A ∧ X ∈ A → trCl X A R ∈ V
4 simp1 ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R → R FrSe A
5 bnj1127 ⊢ y ∈ trCl X A R → y ∈ A
6 5 3ad2ant3 ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R → y ∈ A
7 bnj893 ⊢ R FrSe A ∧ y ∈ A → trCl y A R ∈ V
8 4 6 7 syl2anc ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R → trCl y A R ∈ V
9 8 3expia ⊢ R FrSe A ∧ X ∈ A → y ∈ trCl X A R → trCl y A R ∈ V
10 9 ralrimiv ⊢ R FrSe A ∧ X ∈ A → ∀ y ∈ trCl X A R trCl y A R ∈ V
11 iunexg ⊢ trCl X A R ∈ V ∧ ∀ y ∈ trCl X A R trCl y A R ∈ V → ⋃ y ∈ trCl X A R trCl y A R ∈ V
12 3 10 11 syl2anc ⊢ R FrSe A ∧ X ∈ A → ⋃ y ∈ trCl X A R trCl y A R ∈ V
13 2 12 bnj1149 ⊢ R FrSe A ∧ X ∈ A → pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R ∈ V
14 bnj906 ⊢ R FrSe A ∧ X ∈ A → pred X A R ⊆ trCl X A R
15 iunss1 ⊢ pred X A R ⊆ trCl X A R → ⋃ y ∈ pred X A R trCl y A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
16 unss2 ⊢ ⋃ y ∈ pred X A R trCl y A R ⊆ ⋃ y ∈ trCl X A R trCl y A R → pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R ⊆ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
17 14 15 16 3syl ⊢ R FrSe A ∧ X ∈ A → pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R ⊆ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
18 1 17 eqsstrid ⊢ R FrSe A ∧ X ∈ A → B ⊆ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
19 13 18 ssexd ⊢ R FrSe A ∧ X ∈ A → B ∈ V