Metamath Proof Explorer

Theorem bnj916

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 bnj916.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj916.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj916.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj916.4 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
bnj916.5 ⊢ ( 𝜒 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
Assertion bnj916 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 bnj916.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj916.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj916.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj916.4 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5 bnj916.5 ⊢ ( 𝜒 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
6 bnj256 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
7 6 2exbii ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑛 ∃ 𝑖 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
8 19.41v ⊢ ( ∃ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
9 nfv ⊢ Ⅎ 𝑖 𝑛 ∈ 𝐷
10 1 2 bnj911 ⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∀ 𝑖 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
11 10 nf5i ⊢ Ⅎ 𝑖 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
12 9 11 nfan ⊢ Ⅎ 𝑖 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
13 12 19.42 ⊢ ( ∃ 𝑖 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑛 ∃ 𝑖 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑛 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
15 df-rex ⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
16 df-rex ⊢ ( ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
17 15 16 anbi12i ⊢ ( ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
18 8 14 17 3bitr4i ⊢ ( ∃ 𝑛 ∃ 𝑖 ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
19 7 18 bitri ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
20 19 exbii ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
21 5 3anbi2i ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ) )
22 21 anbi1i ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
23 df-bnj17 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
24 df-bnj17 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ) ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
25 22 23 24 3bitr4i ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
26 25 3exbii ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
27 1 2 3 4 bnj882 ⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
28 27 eleq2i ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ 𝑦 ∈ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
29 eliun ⊢ ( 𝑦 ∈ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ 𝐵 𝑦 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
30 eliun ⊢ ( 𝑦 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
31 30 rexbii ⊢ ( ∃ 𝑓 ∈ 𝐵 𝑦 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
32 28 29 31 3bitri ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) )
33 df-rex ⊢ ( ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
34 4 abeq2i ⊢ ( 𝑓 ∈ 𝐵 ↔ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
35 34 anbi1i ⊢ ( ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
36 35 exbii ⊢ ( ∃ 𝑓 ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
37 32 33 36 3bitri ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
38 20 26 37 3bitr4ri ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
39 bnj643 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) → 𝜒 )
40 5 bnj564 ⊢ ( 𝜒 → dom 𝑓 = 𝑛 )
41 40 eleq2d ⊢ ( 𝜒 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛 ) )
42 anbi1 ⊢ ( ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛 ) → ( ( 𝑖 ∈ dom 𝑓 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝑖 ∈ 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ) )
43 bnj334 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝑓 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
44 bnj252 ⊢ ( ( 𝑖 ∈ dom 𝑓 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝑓 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
45 43 44 bitri ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝑓 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
46 bnj334 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
47 bnj252 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
48 46 47 bitri ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ 𝑛 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
49 42 45 48 3bitr4g ⊢ ( ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛 ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
50 39 41 49 3syl ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
51 50 ibi ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
52 51 2eximi ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) → ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
53 52 eximi ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) → ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
54 38 53 sylbi ⊢ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )