This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
Assertion bnj1413 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )

Proof

Step Hyp Ref Expression
1 bnj1413.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
2 bnj1148 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
3 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
4 simp1 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
5 bnj1127 ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑦 ∈ 𝐴 )
6 5 3ad2ant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ 𝐴 )
7 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
8 4 6 7 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
9 8 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) )
10 9 ralrimiv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
11 iunexg ⊢ ( ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ∧ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
12 3 10 11 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
13 2 12 bnj1149 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∈ V )
14 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
15 iunss1 ⊢ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
16 unss2 ⊢ ( ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
17 14 15 16 3syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
18 1 17 eqsstrid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
19 13 18 ssexd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )