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

Metamath Proof Explorer

Theorem bnj1128

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 bnj1128.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj1128.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1128.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj1128.4 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
bnj1128.5 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj1128.6 ⊢ ( 𝜃 ↔ ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
bnj1128.7 ⊢ ( 𝜏 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜃 ) )
bnj1128.8 ⊢ ( 𝜑′ ↔ [ 𝑗 / 𝑖 ] 𝜑 )
bnj1128.9 ⊢ ( 𝜓′ ↔ [ 𝑗 / 𝑖 ] 𝜓 )
bnj1128.10 ⊢ ( 𝜒′ ↔ [ 𝑗 / 𝑖 ] 𝜒 )
bnj1128.11 ⊢ ( 𝜃′ ↔ [ 𝑗 / 𝑖 ] 𝜃 )
Assertion bnj1128 ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑌 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 bnj1128.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1128.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1128.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj1128.4 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5 bnj1128.5 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
6 bnj1128.6 ⊢ ( 𝜃 ↔ ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
7 bnj1128.7 ⊢ ( 𝜏 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜃 ) )
8 bnj1128.8 ⊢ ( 𝜑′ ↔ [ 𝑗 / 𝑖 ] 𝜑 )
9 bnj1128.9 ⊢ ( 𝜓′ ↔ [ 𝑗 / 𝑖 ] 𝜓 )
10 bnj1128.10 ⊢ ( 𝜒′ ↔ [ 𝑗 / 𝑖 ] 𝜒 )
11 bnj1128.11 ⊢ ( 𝜃′ ↔ [ 𝑗 / 𝑖 ] 𝜃 )
12 1 2 3 4 5 bnj981 ⊢ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) )
13 simp1 ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → 𝜒 )
14 simp2 ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → 𝑖 ∈ 𝑛 )
15 nfv ⊢ Ⅎ 𝑗 𝑖 ∈ 𝑛
16 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜃 )
17 7 16 nfxfr ⊢ Ⅎ 𝑗 𝜏
18 nfv ⊢ Ⅎ 𝑗 𝜒
19 15 17 18 nf3an ⊢ Ⅎ 𝑗 ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 )
20 nfv ⊢ Ⅎ 𝑗 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴
21 19 20 nfim ⊢ Ⅎ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
22 21 nf5ri ⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) → ∀ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
23 3 bnj1098 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
24 simpl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → 𝑖 ≠ ∅ )
25 simpr1 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → 𝑖 ∈ 𝑛 )
26 5 bnj1232 ⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
27 26 3ad2ant3 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → 𝑛 ∈ 𝐷 )
28 27 adantl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → 𝑛 ∈ 𝐷 )
29 24 25 28 3jca ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) )
30 23 29 bnj1101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
31 ancl ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
32 30 31 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) )
33 df-3an ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ↔ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) )
34 33 imbi2i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) ↔ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
35 34 exbii ⊢ ( ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) ↔ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
36 32 35 mpbir ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) )
37 bnj213 ⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
38 37 bnj226 ⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
39 simp21 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝑖 ∈ 𝑛 )
40 simp3r ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝑖 = suc 𝑗 )
41 biid ⊢ ( 𝑛 ∈ 𝐷 ↔ 𝑛 ∈ 𝐷 )
42 biid ⊢ ( 𝑓 Fn 𝑛 ↔ 𝑓 Fn 𝑛 )
43 vex ⊢ 𝑗 ∈ V
44 sbcg ⊢ ( 𝑗 ∈ V → ( [ 𝑗 / 𝑖 ] 𝜑 ↔ 𝜑 ) )
45 43 44 ax-mp ⊢ ( [ 𝑗 / 𝑖 ] 𝜑 ↔ 𝜑 )
46 8 45 bitr2i ⊢ ( 𝜑 ↔ 𝜑′ )
47 2 9 bnj1039 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
48 2 47 bitr4i ⊢ ( 𝜓 ↔ 𝜓′ )
49 41 42 46 48 bnj887 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
50 8 9 5 10 bnj1040 ⊢ ( 𝜒′ ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
51 49 5 50 3bitr4i ⊢ ( 𝜒 ↔ 𝜒′ )
52 50 bnj1254 ⊢ ( 𝜒′ → 𝜓′ )
53 51 52 sylbi ⊢ ( 𝜒 → 𝜓′ )
54 53 3ad2ant3 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → 𝜓′ )
55 54 3ad2ant2 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝜓′ )
56 simp3l ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝑗 ∈ 𝑛 )
57 27 3ad2ant2 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝑛 ∈ 𝐷 )
58 3 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
59 elnn ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑗 ∈ ω )
60 58 59 sylan2 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → 𝑗 ∈ ω )
61 56 57 60 syl2anc ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → 𝑗 ∈ ω )
62 47 bnj589 ⊢ ( 𝜓′ ↔ ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
63 rsp ⊢ ( ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
64 62 63 sylbi ⊢ ( 𝜓′ → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
65 eleq1 ⊢ ( 𝑖 = suc 𝑗 → ( 𝑖 ∈ 𝑛 ↔ suc 𝑗 ∈ 𝑛 ) )
66 fveqeq2 ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
67 65 66 imbi12d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
68 67 imbi2d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑗 ∈ ω → ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
69 64 68 imbitrrid ⊢ ( 𝑖 = suc 𝑗 → ( 𝜓′ → ( 𝑗 ∈ ω → ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
70 40 55 61 69 syl3c ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
71 39 70 mpd ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
72 38 71 bnj1262 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
73 36 72 bnj1023 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
74 5 bnj1247 ⊢ ( 𝜒 → 𝜑 )
75 74 3ad2ant3 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → 𝜑 )
76 bnj213 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
77 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ ∅ ) )
78 1 biimpi ⊢ ( 𝜑 → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
79 77 78 sylan9eq ⊢ ( ( 𝑖 = ∅ ∧ 𝜑 ) → ( 𝑓 ‘ 𝑖 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
80 76 79 bnj1262 ⊢ ( ( 𝑖 = ∅ ∧ 𝜑 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
81 75 80 sylan2 ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
82 73 81 bnj1109 ⊢ ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
83 22 82 bnj1131 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
84 83 3expia ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
85 84 6 sylibr ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )
86 3 5 7 85 bnj1133 ⊢ ( 𝜒 → ∀ 𝑖 ∈ 𝑛 𝜃 )
87 6 ralbii ⊢ ( ∀ 𝑖 ∈ 𝑛 𝜃 ↔ ∀ 𝑖 ∈ 𝑛 ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
88 86 87 sylib ⊢ ( 𝜒 → ∀ 𝑖 ∈ 𝑛 ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
89 rsp ⊢ ( ∀ 𝑖 ∈ 𝑛 ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) → ( 𝑖 ∈ 𝑛 → ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ) )
90 88 89 syl ⊢ ( 𝜒 → ( 𝑖 ∈ 𝑛 → ( 𝜒 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ) )
91 13 14 13 90 syl3c ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
92 simp3 ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) )
93 91 92 sseldd ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → 𝑌 ∈ 𝐴 )
94 93 2eximi ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑌 ∈ ( 𝑓 ‘ 𝑖 ) ) → ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 )
95 12 94 bnj593 ⊢ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 )
96 19.9v ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 ↔ ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 )
97 19.9v ⊢ ( ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 ↔ ∃ 𝑖 𝑌 ∈ 𝐴 )
98 19.9v ⊢ ( ∃ 𝑖 𝑌 ∈ 𝐴 ↔ 𝑌 ∈ 𝐴 )
99 96 97 98 3bitri ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 𝑌 ∈ 𝐴 ↔ 𝑌 ∈ 𝐴 )
100 95 99 sylib ⊢ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑌 ∈ 𝐴 )