Metamath Proof Explorer

Theorem bnj1033

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 bnj1033.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj1033.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1033.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj1033.4 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
bnj1033.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
bnj1033.6 ⊢ ( 𝜂 ↔ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
bnj1033.7 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) )
bnj1033.8 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj1033.9 ⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
bnj1033.10 ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → 𝑧 ∈ 𝐵 )
Assertion bnj1033 ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1033.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1033.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1033.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4 bnj1033.4 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
5 bnj1033.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
6 bnj1033.6 ⊢ ( 𝜂 ↔ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
7 bnj1033.7 ⊢ ( 𝜁 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) )
8 bnj1033.8 ⊢ 𝐷 = ( ω ∖ { ∅ } )
9 bnj1033.9 ⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
10 bnj1033.10 ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → 𝑧 ∈ 𝐵 )
11 1 2 8 9 3 bnj983 ⊢ ( 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) )
12 19.42v ⊢ ( ∃ 𝑖 ( ( 𝜃 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
13 df-3an ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑖 ( ( 𝜃 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
15 df-3an ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
16 12 14 15 3bitr4i ⊢ ( ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
17 16 exbii ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑛 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
18 19.42v ⊢ ( ∃ 𝑛 ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
19 15 exbii ⊢ ( ∃ 𝑛 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑛 ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
20 df-3an ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
21 18 19 20 3bitr4i ⊢ ( ∃ 𝑛 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
22 17 21 bitri ⊢ ( ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
23 22 exbii ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑓 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
24 19.42v ⊢ ( ∃ 𝑓 ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
25 20 exbii ⊢ ( ∃ 𝑓 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑓 ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
26 df-3an ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
27 24 25 26 3bitr4i ⊢ ( ∃ 𝑓 ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
28 23 27 bitri ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
29 bnj255 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) ↔ ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝜁 ) ) )
30 7 anbi2i ⊢ ( ( 𝜒 ∧ 𝜁 ) ↔ ( 𝜒 ∧ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
31 3anass ⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
32 30 31 bitr4i ⊢ ( ( 𝜒 ∧ 𝜁 ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) )
33 32 3anbi3i ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝜁 ) ) ↔ ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
34 29 33 bitri ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) ↔ ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
35 34 3exbii ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
36 35 10 sylbir ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) → 𝑧 ∈ 𝐵 )
37 28 36 sylbir ⊢ ( ( 𝜃 ∧ 𝜏 ∧ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) → 𝑧 ∈ 𝐵 )
38 11 37 syl3an3b ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ 𝐵 )
39 38 3expia ⊢ ( ( 𝜃 ∧ 𝜏 ) → ( 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑧 ∈ 𝐵 ) )
40 39 ssrdv ⊢ ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )