Metamath Proof Explorer


Theorem bnj1121

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 bnj1121.1 ( 𝜃 ↔ ( 𝑅 FrSe 𝐴𝑋𝐴 ) )
bnj1121.2 ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
bnj1121.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
bnj1121.4 ( 𝜁 ↔ ( 𝑖𝑛𝑧 ∈ ( 𝑓𝑖 ) ) )
bnj1121.5 ( 𝜂 ↔ ( ( 𝑓𝐾𝑖 ∈ dom 𝑓 ) → ( 𝑓𝑖 ) ⊆ 𝐵 ) )
bnj1121.6 ( ( 𝜃𝜏𝜒𝜁 ) → ∀ 𝑖𝑛 𝜂 )
bnj1121.7 𝐾 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
Assertion bnj1121 ( ( 𝜃𝜏𝜒𝜁 ) → 𝑧𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1121.1 ( 𝜃 ↔ ( 𝑅 FrSe 𝐴𝑋𝐴 ) )
2 bnj1121.2 ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
3 bnj1121.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
4 bnj1121.4 ( 𝜁 ↔ ( 𝑖𝑛𝑧 ∈ ( 𝑓𝑖 ) ) )
5 bnj1121.5 ( 𝜂 ↔ ( ( 𝑓𝐾𝑖 ∈ dom 𝑓 ) → ( 𝑓𝑖 ) ⊆ 𝐵 ) )
6 bnj1121.6 ( ( 𝜃𝜏𝜒𝜁 ) → ∀ 𝑖𝑛 𝜂 )
7 bnj1121.7 𝐾 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
8 19.8a ( 𝜒 → ∃ 𝑛 𝜒 )
9 8 bnj707 ( ( 𝜃𝜏𝜒𝜁 ) → ∃ 𝑛 𝜒 )
10 3 7 bnj1083 ( 𝑓𝐾 ↔ ∃ 𝑛 𝜒 )
11 9 10 sylibr ( ( 𝜃𝜏𝜒𝜁 ) → 𝑓𝐾 )
12 4 simplbi ( 𝜁𝑖𝑛 )
13 12 bnj708 ( ( 𝜃𝜏𝜒𝜁 ) → 𝑖𝑛 )
14 3 bnj1235 ( 𝜒𝑓 Fn 𝑛 )
15 14 bnj707 ( ( 𝜃𝜏𝜒𝜁 ) → 𝑓 Fn 𝑛 )
16 15 fndmd ( ( 𝜃𝜏𝜒𝜁 ) → dom 𝑓 = 𝑛 )
17 13 16 eleqtrrd ( ( 𝜃𝜏𝜒𝜁 ) → 𝑖 ∈ dom 𝑓 )
18 6 13 bnj1294 ( ( 𝜃𝜏𝜒𝜁 ) → 𝜂 )
19 18 5 sylib ( ( 𝜃𝜏𝜒𝜁 ) → ( ( 𝑓𝐾𝑖 ∈ dom 𝑓 ) → ( 𝑓𝑖 ) ⊆ 𝐵 ) )
20 11 17 19 mp2and ( ( 𝜃𝜏𝜒𝜁 ) → ( 𝑓𝑖 ) ⊆ 𝐵 )
21 4 simprbi ( 𝜁𝑧 ∈ ( 𝑓𝑖 ) )
22 21 bnj708 ( ( 𝜃𝜏𝜒𝜁 ) → 𝑧 ∈ ( 𝑓𝑖 ) )
23 20 22 sseldd ( ( 𝜃𝜏𝜒𝜁 ) → 𝑧𝐵 )