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 )