Metamath Proof Explorer

Theorem bnj1408

Description: Technical lemma for bnj1414 . 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 bnj1408.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
bnj1408.2 ⊢ 𝐶 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
bnj1408.3 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
bnj1408.4 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
Assertion bnj1408 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1408.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
2 bnj1408.2 ⊢ 𝐶 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
3 bnj1408.3 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
4 bnj1408.4 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
5 3 biimpri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝜃 )
6 1 bnj1413 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )
7 simplll ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
8 bnj213 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
9 8 sseli ⊢ ( 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) → 𝑧 ∈ 𝐴 )
10 9 adantl ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ 𝐴 )
11 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
12 7 10 11 syl2anc ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
13 bnj1318 ⊢ ( 𝑦 = 𝑧 → trCl ( 𝑦 , 𝐴 , 𝑅 ) = trCl ( 𝑧 , 𝐴 , 𝑅 ) )
14 13 ssiun2s ⊢ ( 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
15 ssun4 ⊢ ( trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
16 15 1 sseqtrrdi ⊢ ( trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
17 14 16 syl ⊢ ( 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
18 17 adantl ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
19 12 18 sstrd ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
20 simpr ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
21 20 bnj1405 ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
22 biid ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
23 nfv ⊢ Ⅎ 𝑦 ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 )
24 nfcv ⊢ Ⅎ 𝑦 pred ( 𝑋 , 𝐴 , 𝑅 )
25 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 )
26 24 25 nfun ⊢ Ⅎ 𝑦 ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
27 1 26 nfcxfr ⊢ Ⅎ 𝑦 𝐵
28 27 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
29 23 28 nfan ⊢ Ⅎ 𝑦 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 )
30 25 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 )
31 29 30 nfan ⊢ Ⅎ 𝑦 ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
32 31 nf5ri ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∀ 𝑦 ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
33 21 22 32 bnj1521 ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
34 simplll ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
35 34 3ad2ant1 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
36 bnj1147 ⊢ trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
37 simp3 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
38 36 37 bnj1213 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ 𝐴 )
39 35 38 11 syl2anc ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
40 simp2 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) )
41 8 40 bnj1213 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ 𝐴 )
42 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
43 35 41 37 42 syl3anc ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
44 39 43 sstrd ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
45 ssiun2 ⊢ ( 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
46 45 3ad2ant2 ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
47 ssun4 ⊢ ( trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
48 47 1 sseqtrrdi ⊢ ( trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
49 46 48 syl ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
50 44 49 sstrd ⊢ ( ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ∧ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
51 33 50 bnj593 ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
52 nfcv ⊢ Ⅎ 𝑦 pred ( 𝑧 , 𝐴 , 𝑅 )
53 52 27 nfss ⊢ Ⅎ 𝑦 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵
54 53 nf5ri ⊢ ( pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 → ∀ 𝑦 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
55 51 54 bnj1397 ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
56 simpr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
57 1 bnj1138 ⊢ ( 𝑧 ∈ 𝐵 ↔ ( 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
58 56 57 sylib ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
59 19 55 58 mpjaodan ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
60 59 ralrimiva ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐵 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
61 df-bnj19 ⊢ ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∀ 𝑧 ∈ 𝐵 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
62 60 61 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )
63 1 bnj931 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵
64 63 a1i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
65 6 62 64 4 syl3anbrc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝜏 )
66 3 4 bnj1124 ⊢ ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
67 5 65 66 syl2anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
68 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
69 iunss1 ⊢ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
70 unss2 ⊢ ( ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
71 68 69 70 3syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
72 71 1 2 3sstr4g ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
73 biid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
74 biid ⊢ ( ( 𝐶 ∈ V ∧ TrFo ( 𝐶 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐶 ) ↔ ( 𝐶 ∈ V ∧ TrFo ( 𝐶 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐶 ) )
75 2 73 74 bnj1136 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝐶 )
76 72 75 sseqtrrd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
77 67 76 eqssd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) = 𝐵 )