Metamath Proof Explorer


Theorem bnj66

Description: Technical lemma for bnj60 . 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 bnj66.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj66.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj66.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
Assertion bnj66 ( 𝑔𝐶 → Rel 𝑔 )

Proof

Step Hyp Ref Expression
1 bnj66.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj66.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj66.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
4 fneq1 ( 𝑔 = 𝑓 → ( 𝑔 Fn 𝑑𝑓 Fn 𝑑 ) )
5 fveq1 ( 𝑔 = 𝑓 → ( 𝑔𝑥 ) = ( 𝑓𝑥 ) )
6 reseq1 ( 𝑔 = 𝑓 → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
7 6 opeq2d ( 𝑔 = 𝑓 → ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ )
8 7 2 eqtr4di ( 𝑔 = 𝑓 → ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = 𝑌 )
9 8 fveq2d ( 𝑔 = 𝑓 → ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺𝑌 ) )
10 5 9 eqeq12d ( 𝑔 = 𝑓 → ( ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) )
11 10 ralbidv ( 𝑔 = 𝑓 → ( ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) )
12 4 11 anbi12d ( 𝑔 = 𝑓 → ( ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ) )
13 12 rexbidv ( 𝑔 = 𝑓 → ( ∃ 𝑑𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ) )
14 13 cbvabv { 𝑔 ∣ ∃ 𝑑𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
15 3 14 eqtr4i 𝐶 = { 𝑔 ∣ ∃ 𝑑𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
16 15 bnj1436 ( 𝑔𝐶 → ∃ 𝑑𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
17 bnj1239 ( ∃ 𝑑𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑔𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) → ∃ 𝑑𝐵 𝑔 Fn 𝑑 )
18 fnrel ( 𝑔 Fn 𝑑 → Rel 𝑔 )
19 18 rexlimivw ( ∃ 𝑑𝐵 𝑔 Fn 𝑑 → Rel 𝑔 )
20 16 17 19 3syl ( 𝑔𝐶 → Rel 𝑔 )