Metamath Proof Explorer

Theorem bnj1137

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bnj1137.1 ⊢ B = pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
2 1 eleq2i ⊢ v ∈ B ↔ v ∈ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
3 elun ⊢ v ∈ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R ↔ v ∈ pred X A R ∨ v ∈ ⋃ y ∈ trCl X A R trCl y A R
4 2 3 bitri ⊢ v ∈ B ↔ v ∈ pred X A R ∨ v ∈ ⋃ y ∈ trCl X A R trCl y A R
5 bnj213 ⊢ pred X A R ⊆ A
6 5 sseli ⊢ v ∈ pred X A R → v ∈ A
7 bnj906 ⊢ R FrSe A ∧ v ∈ A → pred v A R ⊆ trCl v A R
8 7 adantlr ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ A → pred v A R ⊆ trCl v A R
9 6 8 sylan2 ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R → pred v A R ⊆ trCl v A R
10 bnj906 ⊢ R FrSe A ∧ X ∈ A → pred X A R ⊆ trCl X A R
11 10 sselda ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R → v ∈ trCl X A R
12 bnj18eq1 ⊢ y = v → trCl y A R = trCl v A R
13 12 ssiun2s ⊢ v ∈ trCl X A R → trCl v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
14 11 13 syl ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R → trCl v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
15 9 14 sstrd ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R → pred v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
16 bnj1147 ⊢ trCl y A R ⊆ A
17 16 rgenw ⊢ ∀ y ∈ trCl X A R trCl y A R ⊆ A
18 iunss ⊢ ⋃ y ∈ trCl X A R trCl y A R ⊆ A ↔ ∀ y ∈ trCl X A R trCl y A R ⊆ A
19 17 18 mpbir ⊢ ⋃ y ∈ trCl X A R trCl y A R ⊆ A
20 19 sseli ⊢ v ∈ ⋃ y ∈ trCl X A R trCl y A R → v ∈ A
21 20 8 sylan2 ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ ⋃ y ∈ trCl X A R trCl y A R → pred v A R ⊆ trCl v A R
22 bnj1125 ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R → trCl y A R ⊆ trCl X A R
23 22 3expia ⊢ R FrSe A ∧ X ∈ A → y ∈ trCl X A R → trCl y A R ⊆ trCl X A R
24 23 ralrimiv ⊢ R FrSe A ∧ X ∈ A → ∀ y ∈ trCl X A R trCl y A R ⊆ trCl X A R
25 iunss ⊢ ⋃ y ∈ trCl X A R trCl y A R ⊆ trCl X A R ↔ ∀ y ∈ trCl X A R trCl y A R ⊆ trCl X A R
26 24 25 sylibr ⊢ R FrSe A ∧ X ∈ A → ⋃ y ∈ trCl X A R trCl y A R ⊆ trCl X A R
27 26 sselda ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ ⋃ y ∈ trCl X A R trCl y A R → v ∈ trCl X A R
28 27 13 syl ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ ⋃ y ∈ trCl X A R trCl y A R → trCl v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
29 21 28 sstrd ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ ⋃ y ∈ trCl X A R trCl y A R → pred v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
30 15 29 jaodan ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R ∨ v ∈ ⋃ y ∈ trCl X A R trCl y A R → pred v A R ⊆ ⋃ y ∈ trCl X A R trCl y A R
31 ssun2 ⊢ ⋃ y ∈ trCl X A R trCl y A R ⊆ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
32 31 1 sseqtrri ⊢ ⋃ y ∈ trCl X A R trCl y A R ⊆ B
33 30 32 sstrdi ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ pred X A R ∨ v ∈ ⋃ y ∈ trCl X A R trCl y A R → pred v A R ⊆ B
34 4 33 sylan2b ⊢ R FrSe A ∧ X ∈ A ∧ v ∈ B → pred v A R ⊆ B
35 34 ralrimiva ⊢ R FrSe A ∧ X ∈ A → ∀ v ∈ B pred v A R ⊆ B
36 df-bnj19 ⊢ TrFo B A R ↔ ∀ v ∈ B pred v A R ⊆ B
37 35 36 sylibr ⊢ R FrSe A ∧ X ∈ A → TrFo B A R