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=predXAR∪⋃y∈predXARtrClyAR
Assertion bnj1413 ⊢RFrSeA∧X∈A→B∈V

Proof

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