Metamath Proof Explorer

Theorem bnj1029

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

Ref Expression
Assertion bnj1029 ⊢RFrSeA∧X∈A→TrFotrClXARAR

Proof

Step Hyp Ref Expression
1 biid ⊢f⁡∅=predXAR↔f⁡∅=predXAR
2 biid ⊢∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
3 biid ⊢n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
4 biid ⊢RFrSeA∧X∈A∧y∈trClXAR∧z∈predyAR↔RFrSeA∧X∈A∧y∈trClXAR∧z∈predyAR
5 biid ⊢m∈ω∧n=suc⁡m∧p=suc⁡n↔m∈ω∧n=suc⁡m∧p=suc⁡n
6 biid ⊢i∈n∧y∈f⁡i↔i∈n∧y∈f⁡i
7 biid ⊢[˙p/n]˙f⁡∅=predXAR↔[˙p/n]˙f⁡∅=predXAR
8 biid ⊢[˙p/n]˙∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔[˙p/n]˙∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
9 biid ⊢[˙p/n]˙n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔[˙p/n]˙n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
10 biid ⊢[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙f⁡∅=predXAR↔[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙f⁡∅=predXAR
11 biid ⊢[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
12 biid ⊢[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR↔[˙f∪n⋃y∈f⁡mpredyAR/f]˙[˙p/n]˙n∈ω∖∅∧fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
13 eqid ⊢ω∖∅=ω∖∅
14 eqid ⊢f|∃n∈ω∖∅fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR=f|∃n∈ω∖∅fFnn∧f⁡∅=predXAR∧∀i∈ωsuc⁡i∈n→f⁡suc⁡i=⋃y∈f⁡ipredyAR
15 eqid ⊢⋃y∈f⁡mpredyAR=⋃y∈f⁡mpredyAR
16 eqid ⊢f∪n⋃y∈f⁡mpredyAR=f∪n⋃y∈f⁡mpredyAR
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 bnj907 ⊢RFrSeA∧X∈A→TrFotrClXARAR