Metamath Proof Explorer

Theorem bnj1280

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

Proof

Step Hyp Ref Expression
1 bnj1280.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1280.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1280.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1280.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5 bnj1280.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6 bnj1280.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7 bnj1280.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1280.17 ⊢ ( 𝜓 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )
9 1 2 3 4 5 6 7 bnj1286 ⊢ ( 𝜓 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐷 )
10 9 sseld ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑧 ∈ 𝐷 ) )
11 disj1 ⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ ↔ ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐸 ) )
12 8 11 sylib ⊢ ( 𝜓 → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐸 ) )
13 12 19.21bi ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐸 ) )
14 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑧 ) )
15 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑧 ) )
16 14 15 neeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ↔ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) )
17 16 5 elrab2 ⊢ ( 𝑧 ∈ 𝐸 ↔ ( 𝑧 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) )
18 17 notbii ⊢ ( ¬ 𝑧 ∈ 𝐸 ↔ ¬ ( 𝑧 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) )
19 imnan ⊢ ( ( 𝑧 ∈ 𝐷 → ¬ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) ↔ ¬ ( 𝑧 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) )
20 nne ⊢ ( ¬ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ↔ ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) )
21 20 imbi2i ⊢ ( ( 𝑧 ∈ 𝐷 → ¬ ( 𝑔 ‘ 𝑧 ) ≠ ( ℎ ‘ 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐷 → ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) ) )
22 18 19 21 3bitr2i ⊢ ( ¬ 𝑧 ∈ 𝐸 ↔ ( 𝑧 ∈ 𝐷 → ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) ) )
23 13 22 syl6ib ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ 𝐷 → ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) ) ) )
24 10 23 mpdd ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) ) )
25 24 imp ⊢ ( ( 𝜓 ∧ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( 𝑔 ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) )
26 fvres ⊢ ( 𝑧 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
27 10 26 syl6 ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ) )
28 27 imp ⊢ ( ( 𝜓 ∧ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
29 fvres ⊢ ( 𝑧 ∈ 𝐷 → ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) )
30 10 29 syl6 ⊢ ( 𝜓 → ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) ) )
31 30 imp ⊢ ( ( 𝜓 ∧ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) = ( ℎ ‘ 𝑧 ) )
32 25 28 31 3eqtr4d ⊢ ( ( 𝜓 ∧ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) )
33 32 ralrimiva ⊢ ( 𝜓 → ∀ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) )
34 9 resabs1d ⊢ ( 𝜓 → ( ( 𝑔 ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
35 9 resabs1d ⊢ ( 𝜓 → ( ( ℎ ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
36 34 35 eqeq12d ⊢ ( 𝜓 → ( ( ( 𝑔 ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ( ℎ ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ↔ ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
37 1 2 3 4 5 6 7 bnj1256 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 𝑔 Fn 𝑑 )
38 4 bnj1292 ⊢ 𝐷 ⊆ dom 𝑔
39 fndm ⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
40 38 39 sseqtrid ⊢ ( 𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑 )
41 fnssres ⊢ ( ( 𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑 ) → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
42 40 41 mpdan ⊢ ( 𝑔 Fn 𝑑 → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
43 37 42 bnj31 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
44 43 bnj1265 ⊢ ( 𝜑 → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
45 7 44 bnj835 ⊢ ( 𝜓 → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
46 1 2 3 4 5 6 7 bnj1259 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 )
47 4 bnj1293 ⊢ 𝐷 ⊆ dom ℎ
48 fndm ⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
49 47 48 sseqtrid ⊢ ( ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑 )
50 fnssres ⊢ ( ( ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑 ) → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
51 49 50 mpdan ⊢ ( ℎ Fn 𝑑 → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
52 46 51 bnj31 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ( ℎ ↾ 𝐷 ) Fn 𝐷 )
53 52 bnj1265 ⊢ ( 𝜑 → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
54 7 53 bnj835 ⊢ ( 𝜓 → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
55 fvreseq ⊢ ( ( ( ( 𝑔 ↾ 𝐷 ) Fn 𝐷 ∧ ( ℎ ↾ 𝐷 ) Fn 𝐷 ) ∧ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐷 ) → ( ( ( 𝑔 ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ( ℎ ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) ) )
56 45 54 9 55 syl21anc ⊢ ( 𝜓 → ( ( ( 𝑔 ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ( ℎ ↾ 𝐷 ) ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) ) )
57 36 56 bitr3d ⊢ ( 𝜓 → ( ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑧 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑧 ) ) )
58 33 57 mpbird ⊢ ( 𝜓 → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )