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

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 𝑔 )