Metamath Proof Explorer

Theorem bnj1136

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1136.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
bnj1136.2 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
bnj1136.3 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
Assertion bnj1136 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1136.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
2 bnj1136.2 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
3 bnj1136.3 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
4 2 biimpri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝜃 )
5 bnj1148 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
6 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
7 simp1 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
8 bnj1127 ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑦 ∈ 𝐴 )
9 8 3ad2ant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ 𝐴 )
10 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
11 7 9 10 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
12 11 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) )
13 12 ralrimiv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
14 iunexg ⊢ ( ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ∧ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
15 6 13 14 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
16 5 15 bnj1149 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∈ V )
17 1 16 eqeltrid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )
18 1 bnj1137 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )
19 1 bnj931 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵
20 19 a1i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
21 17 18 20 3 syl3anbrc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝜏 )
22 2 3 bnj1124 ⊢ ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
23 4 21 22 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
24 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
25 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
26 25 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
27 26 ralrimiv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
28 ss2iun ⊢ ( ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑋 , 𝐴 , 𝑅 ) )
29 bnj1143 ⊢ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 )
30 28 29 sstrdi ⊢ ( ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
31 27 30 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
32 24 31 unssd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
33 1 32 eqsstrid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
34 23 33 eqssd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝐵 )