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

Metamath Proof Explorer

Theorem bnj1501

Description: Technical lemma for bnj1500 . 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 bnj1501.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1501.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1501.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1501.4 ⊢ 𝐹 = ∪ 𝐶
bnj1501.5 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
bnj1501.6 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓 ) )
bnj1501.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑 ) )
Assertion bnj1501 ( 𝑅 FrSe 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 bnj1501.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1501.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1501.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1501.4 ⊢ 𝐹 = ∪ 𝐶
5 bnj1501.5 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
6 bnj1501.6 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓 ) )
7 bnj1501.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑 ) )
8 5 simprbi ⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
9 1 2 3 4 bnj60 ⊢ ( 𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴 )
10 9 fndmd ⊢ ( 𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴 )
11 5 10 bnj832 ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
12 8 11 eleqtrrd ⊢ ( 𝜑 → 𝑥 ∈ dom 𝐹 )
13 4 dmeqi ⊢ dom 𝐹 = dom ∪ 𝐶
14 3 bnj1317 ⊢ ( 𝑤 ∈ 𝐶 → ∀ 𝑓 𝑤 ∈ 𝐶 )
15 14 bnj1400 ⊢ dom ∪ 𝐶 = ∪ 𝑓 ∈ 𝐶 dom 𝑓
16 13 15 eqtri ⊢ dom 𝐹 = ∪ 𝑓 ∈ 𝐶 dom 𝑓
17 12 16 eleqtrdi ⊢ ( 𝜑 → 𝑥 ∈ ∪ 𝑓 ∈ 𝐶 dom 𝑓 )
18 17 bnj1405 ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓 )
19 18 6 bnj1209 ⊢ ( 𝜑 → ∃ 𝑓 𝜓 )
20 3 bnj1436 ⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
21 20 bnj1299 ⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 𝑓 Fn 𝑑 )
22 fndm ⊢ ( 𝑓 Fn 𝑑 → dom 𝑓 = 𝑑 )
23 21 22 bnj31 ⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 dom 𝑓 = 𝑑 )
24 6 23 bnj836 ⊢ ( 𝜓 → ∃ 𝑑 ∈ 𝐵 dom 𝑓 = 𝑑 )
25 1 2 3 4 5 6 bnj1518 ⊢ ( 𝜓 → ∀ 𝑑 𝜓 )
26 24 7 25 bnj1521 ⊢ ( 𝜓 → ∃ 𝑑 𝜒 )
27 9 fnfund ⊢ ( 𝑅 FrSe 𝐴 → Fun 𝐹 )
28 5 27 bnj832 ⊢ ( 𝜑 → Fun 𝐹 )
29 6 28 bnj835 ⊢ ( 𝜓 → Fun 𝐹 )
30 elssuni ⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ⊆ ∪ 𝐶 )
31 30 4 sseqtrrdi ⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ⊆ 𝐹 )
32 6 31 bnj836 ⊢ ( 𝜓 → 𝑓 ⊆ 𝐹 )
33 6 simp3bi ⊢ ( 𝜓 → 𝑥 ∈ dom 𝑓 )
34 29 32 33 bnj1502 ⊢ ( 𝜓 → ( 𝐹 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
35 1 2 3 bnj1514 ⊢ ( 𝑓 ∈ 𝐶 → ∀ 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
36 6 35 bnj836 ⊢ ( 𝜓 → ∀ 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
37 36 33 bnj1294 ⊢ ( 𝜓 → ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
38 34 37 eqtrd ⊢ ( 𝜓 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
39 7 38 bnj835 ⊢ ( 𝜒 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
40 7 29 bnj835 ⊢ ( 𝜒 → Fun 𝐹 )
41 7 32 bnj835 ⊢ ( 𝜒 → 𝑓 ⊆ 𝐹 )
42 1 bnj1517 ⊢ ( 𝑑 ∈ 𝐵 → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
43 7 42 bnj836 ⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
44 7 33 bnj835 ⊢ ( 𝜒 → 𝑥 ∈ dom 𝑓 )
45 7 simp3bi ⊢ ( 𝜒 → dom 𝑓 = 𝑑 )
46 44 45 eleqtrd ⊢ ( 𝜒 → 𝑥 ∈ 𝑑 )
47 43 46 bnj1294 ⊢ ( 𝜒 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
48 47 45 sseqtrrd ⊢ ( 𝜒 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑓 )
49 40 41 48 bnj1503 ⊢ ( 𝜒 → ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
50 49 opeq2d ⊢ ( 𝜒 → ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ )
51 50 2 eqtr4di ⊢ ( 𝜒 → ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = 𝑌 )
52 51 fveq2d ⊢ ( 𝜒 → ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺 ‘ 𝑌 ) )
53 39 52 eqtr4d ⊢ ( 𝜒 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
54 26 53 bnj593 ⊢ ( 𝜓 → ∃ 𝑑 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
55 1 2 3 4 bnj1519 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) → ∀ 𝑑 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
56 54 55 bnj1397 ⊢ ( 𝜓 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
57 19 56 bnj593 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
58 1 2 3 4 bnj1520 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) → ∀ 𝑓 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
59 57 58 bnj1397 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
60 5 59 bnj1459 ⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )