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

Metamath Proof Explorer

Theorem bnj1296

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 bnj1296.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1296.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1296.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1296.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
bnj1296.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
bnj1296.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
bnj1296.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
bnj1296.18 ⊢ ( 𝜓 → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
bnj1296.9 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1296.10 ⊢ 𝐾 = { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) }
bnj1296.11 ⊢ 𝑊 = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1296.12 ⊢ 𝐿 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) }
Assertion bnj1296 ( 𝜓 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 bnj1296.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1296.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1296.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1296.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5 bnj1296.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6 bnj1296.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7 bnj1296.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1296.18 ⊢ ( 𝜓 → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
9 bnj1296.9 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
10 bnj1296.10 ⊢ 𝐾 = { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) }
11 bnj1296.11 ⊢ 𝑊 = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12 bnj1296.12 ⊢ 𝐿 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) }
13 8 opeq2d ⊢ ( 𝜓 → ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ )
14 13 9 11 3eqtr4g ⊢ ( 𝜓 → 𝑍 = 𝑊 )
15 14 fveq2d ⊢ ( 𝜓 → ( 𝐺 ‘ 𝑍 ) = ( 𝐺 ‘ 𝑊 ) )
16 10 bnj1436 ⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
17 fndm ⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
18 17 anim1i ⊢ ( ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) → ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
19 16 18 bnj31 ⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
20 raleq ⊢ ( dom 𝑔 = 𝑑 → ( ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ↔ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
21 20 pm5.32i ⊢ ( ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) ↔ ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
22 21 rexbii ⊢ ( ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
23 19 22 sylibr ⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
24 simpr ⊢ ( ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
25 23 24 bnj31 ⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
26 25 bnj1265 ⊢ ( 𝑔 ∈ 𝐾 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
27 2 3 9 10 bnj1234 ⊢ 𝐶 = 𝐾
28 26 27 eleq2s ⊢ ( 𝑔 ∈ 𝐶 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
29 6 28 bnj770 ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
30 7 29 bnj835 ⊢ ( 𝜓 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
31 4 bnj1292 ⊢ 𝐷 ⊆ dom 𝑔
32 5 7 bnj1212 ⊢ ( 𝜓 → 𝑥 ∈ 𝐷 )
33 31 32 bnj1213 ⊢ ( 𝜓 → 𝑥 ∈ dom 𝑔 )
34 30 33 bnj1294 ⊢ ( 𝜓 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
35 12 bnj1436 ⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
36 fndm ⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
37 36 anim1i ⊢ ( ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) → ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
38 35 37 bnj31 ⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
39 raleq ⊢ ( dom ℎ = 𝑑 → ( ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ↔ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
40 39 pm5.32i ⊢ ( ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
41 40 rexbii ⊢ ( ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
42 38 41 sylibr ⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
43 simpr ⊢ ( ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
44 42 43 bnj31 ⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
45 44 bnj1265 ⊢ ( ℎ ∈ 𝐿 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
46 2 3 11 12 bnj1234 ⊢ 𝐶 = 𝐿
47 45 46 eleq2s ⊢ ( ℎ ∈ 𝐶 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
48 6 47 bnj771 ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
49 7 48 bnj835 ⊢ ( 𝜓 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
50 4 bnj1293 ⊢ 𝐷 ⊆ dom ℎ
51 50 32 bnj1213 ⊢ ( 𝜓 → 𝑥 ∈ dom ℎ )
52 49 51 bnj1294 ⊢ ( 𝜓 → ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
53 15 34 52 3eqtr4d ⊢ ( 𝜓 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )