Metamath Proof Explorer

Theorem bnj1145

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

Proof

Step Hyp Ref Expression
1 bnj1145.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1145.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1145.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj1145.4 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5 bnj1145.5 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
6 bnj1145.6 ⊢ ( 𝜃 ↔ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) )
7 1 2 3 4 bnj882 ⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
8 ss2iun ⊢ ( ∀ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 → ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴 )
9 5 4 bnj1083 ⊢ ( 𝑓 ∈ 𝐵 ↔ ∃ 𝑛 𝜒 )
10 2 bnj1095 ⊢ ( 𝜓 → ∀ 𝑖 𝜓 )
11 10 5 bnj1096 ⊢ ( 𝜒 → ∀ 𝑖 𝜒 )
12 3 bnj1098 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
13 5 bnj1232 ⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
14 13 3anim3i ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) )
15 12 14 bnj1101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
16 ancl ⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
17 15 16 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) )
18 6 imbi2i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
19 18 exbii ⊢ ( ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝜃 ) ↔ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ) ) )
20 17 19 mpbir ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝜃 )
21 bnj213 ⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
22 21 bnj226 ⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
23 simpr ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) → 𝑖 = suc 𝑗 )
24 6 23 simplbiim ⊢ ( 𝜃 → 𝑖 = suc 𝑗 )
25 simp2 ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝑖 ∈ 𝑛 )
26 13 3ad2ant3 ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝑛 ∈ 𝐷 )
27 3 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
28 elnn ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑖 ∈ ω )
29 27 28 sylan2 ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → 𝑖 ∈ ω )
30 25 26 29 syl2anc ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → 𝑖 ∈ ω )
31 6 30 bnj832 ⊢ ( 𝜃 → 𝑖 ∈ ω )
32 vex ⊢ 𝑗 ∈ V
33 32 bnj216 ⊢ ( 𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖 )
34 elnn ⊢ ( ( 𝑗 ∈ 𝑖 ∧ 𝑖 ∈ ω ) → 𝑗 ∈ ω )
35 33 34 sylan ⊢ ( ( 𝑖 = suc 𝑗 ∧ 𝑖 ∈ ω ) → 𝑗 ∈ ω )
36 24 31 35 syl2anc ⊢ ( 𝜃 → 𝑗 ∈ ω )
37 6 25 bnj832 ⊢ ( 𝜃 → 𝑖 ∈ 𝑛 )
38 24 37 eqeltrrd ⊢ ( 𝜃 → suc 𝑗 ∈ 𝑛 )
39 2 bnj589 ⊢ ( 𝜓 ↔ ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
40 39 biimpi ⊢ ( 𝜓 → ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
41 40 bnj708 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
42 rsp ⊢ ( ∀ 𝑗 ∈ ω ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
43 41 42 syl ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
44 5 43 sylbi ⊢ ( 𝜒 → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
45 44 3ad2ant3 ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
46 6 45 bnj832 ⊢ ( 𝜃 → ( 𝑗 ∈ ω → ( suc 𝑗 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
47 36 38 46 mp2d ⊢ ( 𝜃 → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
48 fveqeq2 ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
49 24 48 syl ⊢ ( 𝜃 → ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
50 47 49 mpbird ⊢ ( 𝜃 → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
51 22 50 bnj1262 ⊢ ( 𝜃 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
52 20 51 bnj1023 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
53 3anass ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) ↔ ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) ) )
54 53 imbi1i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ↔ ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
55 54 exbii ⊢ ( ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ↔ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
56 52 55 mpbi ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
57 1 biimpi ⊢ ( 𝜑 → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
58 5 57 bnj771 ⊢ ( 𝜒 → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
59 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ ∅ ) )
60 bnj213 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
61 sseq1 ⊢ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) → ( ( 𝑓 ‘ ∅ ) ⊆ 𝐴 ↔ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴 ) )
62 60 61 mpbiri ⊢ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑓 ‘ ∅ ) ⊆ 𝐴 )
63 sseq1 ⊢ ( ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ ∅ ) → ( ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ↔ ( 𝑓 ‘ ∅ ) ⊆ 𝐴 ) )
64 63 biimpar ⊢ ( ( ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ ∅ ) ∧ ( 𝑓 ‘ ∅ ) ⊆ 𝐴 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
65 59 62 64 syl2an ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
66 58 65 sylan2 ⊢ ( ( 𝑖 = ∅ ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
67 66 adantrl ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
68 56 67 bnj1109 ⊢ ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
69 19.9v ⊢ ( ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
70 68 69 mpbi ⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜒 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
71 70 expcom ⊢ ( 𝜒 → ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
72 fndm ⊢ ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
73 5 72 bnj770 ⊢ ( 𝜒 → dom 𝑓 = 𝑛 )
74 eleq2 ⊢ ( dom 𝑓 = 𝑛 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛 ) )
75 74 imbi1d ⊢ ( dom 𝑓 = 𝑛 → ( ( 𝑖 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ↔ ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ) )
76 73 75 syl ⊢ ( 𝜒 → ( ( 𝑖 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ↔ ( 𝑖 ∈ 𝑛 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) ) )
77 71 76 mpbird ⊢ ( 𝜒 → ( 𝑖 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 ) )
78 11 77 hbralrimi ⊢ ( 𝜒 → ∀ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
79 78 exlimiv ⊢ ( ∃ 𝑛 𝜒 → ∀ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
80 9 79 sylbi ⊢ ( 𝑓 ∈ 𝐵 → ∀ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
81 ss2iun ⊢ ( ∀ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ dom 𝑓 𝐴 )
82 bnj1143 ⊢ ∪ 𝑖 ∈ dom 𝑓 𝐴 ⊆ 𝐴
83 81 82 sstrdi ⊢ ( ∀ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 → ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
84 80 83 syl ⊢ ( 𝑓 ∈ 𝐵 → ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴 )
85 8 84 mprg ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ ∪ 𝑓 ∈ 𝐵 𝐴
86 4 bnj1317 ⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑓 𝑤 ∈ 𝐵 )
87 86 bnj1146 ⊢ ∪ 𝑓 ∈ 𝐵 𝐴 ⊆ 𝐴
88 85 87 sstri ⊢ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ⊆ 𝐴
89 7 88 eqsstri ⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴