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 syl5ibr ( 𝑖 = 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 ( 𝑋 , 𝐴 , 𝑅 ) → 𝑌𝐴 )