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

Metamath Proof Explorer

Theorem bnj1097

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 bnj1097.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj1097.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj1097.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
Assertion bnj1097 ( ( 𝑖 = ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1097.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj1097.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
3 bnj1097.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
4 1 biimpi ⊢ ( 𝜑 → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
5 2 4 bnj771 ⊢ ( 𝜒 → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
6 5 3ad2ant3 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
7 6 adantr ⊢ ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
8 3 simp3bi ⊢ ( 𝜏 → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
9 8 3ad2ant2 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
10 9 adantr ⊢ ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
11 7 10 jca ⊢ ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
12 11 anim2i ⊢ ( ( 𝑖 = ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑖 = ∅ ∧ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) ) )
13 3anass ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) ↔ ( 𝑖 = ∅ ∧ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) ) )
14 12 13 sylibr ⊢ ( ( 𝑖 = ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
15 fveqeq2 ⊢ ( 𝑖 = ∅ → ( ( 𝑓 ‘ 𝑖 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) )
16 15 biimpar ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑓 ‘ 𝑖 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
17 16 adantr ⊢ ( ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) → ( 𝑓 ‘ 𝑖 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
18 simpr ⊢ ( ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
19 17 18 eqsstrd ⊢ ( ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
20 19 3impa ⊢ ( ( 𝑖 = ∅ ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
21 14 20 syl ⊢ ( ( 𝑖 = ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )