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 ) ) → ( 𝑓𝑖 ) ⊆ 𝐵 )