Metamath Proof Explorer

Theorem bnj1450

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 bnj1450.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1450.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1450.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1450.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
bnj1450.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
bnj1450.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
bnj1450.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
bnj1450.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
bnj1450.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
bnj1450.10 ⊢ 𝑃 = ∪ 𝐻
bnj1450.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1450.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
bnj1450.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
bnj1450.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
bnj1450.15 ⊢ ( 𝜒 → 𝑃 Fn trCl ( 𝑥 , 𝐴 , 𝑅 ) )
bnj1450.16 ⊢ ( 𝜒 → 𝑄 Fn ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
bnj1450.17 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) )
bnj1450.18 ⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑧 ∈ { 𝑥 } ) )
bnj1450.19 ⊢ ( 𝜁 ↔ ( 𝜃 ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
bnj1450.20 ⊢ ( 𝜌 ↔ ( 𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
bnj1450.21 ⊢ ( 𝜎 ↔ ( 𝜌 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
bnj1450.22 ⊢ ( 𝜑 ↔ ( 𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
bnj1450.23 ⊢ 𝑋 = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
Assertion bnj1450 ( 𝜁 → ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 bnj1450.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1450.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1450.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1450.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1450.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1450.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
7 bnj1450.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1450.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1450.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1450.10 ⊢ 𝑃 = ∪ 𝐻
11 bnj1450.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12 bnj1450.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
13 bnj1450.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
14 bnj1450.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
15 bnj1450.15 ⊢ ( 𝜒 → 𝑃 Fn trCl ( 𝑥 , 𝐴 , 𝑅 ) )
16 bnj1450.16 ⊢ ( 𝜒 → 𝑄 Fn ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
17 bnj1450.17 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) )
18 bnj1450.18 ⊢ ( 𝜂 ↔ ( 𝜃 ∧ 𝑧 ∈ { 𝑥 } ) )
19 bnj1450.19 ⊢ ( 𝜁 ↔ ( 𝜃 ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
20 bnj1450.20 ⊢ ( 𝜌 ↔ ( 𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓 ) )
21 bnj1450.21 ⊢ ( 𝜎 ↔ ( 𝜌 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
22 bnj1450.22 ⊢ ( 𝜑 ↔ ( 𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
23 bnj1450.23 ⊢ 𝑋 = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
24 19 simprbi ⊢ ( 𝜁 → 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
25 15 fndmd ⊢ ( 𝜒 → dom 𝑃 = trCl ( 𝑥 , 𝐴 , 𝑅 ) )
26 17 25 bnj832 ⊢ ( 𝜃 → dom 𝑃 = trCl ( 𝑥 , 𝐴 , 𝑅 ) )
27 19 26 bnj832 ⊢ ( 𝜁 → dom 𝑃 = trCl ( 𝑥 , 𝐴 , 𝑅 ) )
28 24 27 eleqtrrd ⊢ ( 𝜁 → 𝑧 ∈ dom 𝑃 )
29 10 dmeqi ⊢ dom 𝑃 = dom ∪ 𝐻
30 28 29 eleqtrdi ⊢ ( 𝜁 → 𝑧 ∈ dom ∪ 𝐻 )
31 9 bnj1317 ⊢ ( 𝑤 ∈ 𝐻 → ∀ 𝑓 𝑤 ∈ 𝐻 )
32 31 bnj1400 ⊢ dom ∪ 𝐻 = ∪ 𝑓 ∈ 𝐻 dom 𝑓
33 30 32 eleqtrdi ⊢ ( 𝜁 → 𝑧 ∈ ∪ 𝑓 ∈ 𝐻 dom 𝑓 )
34 33 bnj1405 ⊢ ( 𝜁 → ∃ 𝑓 ∈ 𝐻 𝑧 ∈ dom 𝑓 )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 bnj1449 ⊢ ( 𝜁 → ∀ 𝑓 𝜁 )
36 34 20 35 bnj1521 ⊢ ( 𝜁 → ∃ 𝑓 𝜌 )
37 9 bnj1436 ⊢ ( 𝑓 ∈ 𝐻 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ )
38 20 37 bnj836 ⊢ ( 𝜌 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ )
39 1 2 3 4 8 bnj1373 ⊢ ( 𝜏′ ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
40 39 rexbii ⊢ ( ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
41 38 40 sylib ⊢ ( 𝜌 → ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
42 41 bnj1196 ⊢ ( 𝜌 → ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
43 3anass ⊢ ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
44 42 43 bnj1198 ⊢ ( 𝜌 → ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
45 bnj252 ⊢ ( ( 𝜌 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝜌 ∧ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
46 21 45 bitri ⊢ ( 𝜎 ↔ ( 𝜌 ∧ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑦 } ∪ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 bnj1444 ⊢ ( 𝜌 → ∀ 𝑦 𝜌 )
48 44 46 47 bnj1340 ⊢ ( 𝜌 → ∃ 𝑦 𝜎 )
49 3 bnj1436 ⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
50 21 49 bnj771 ⊢ ( 𝜎 → ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
51 50 bnj1196 ⊢ ( 𝜎 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
52 3anass ⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ↔ ( 𝑑 ∈ 𝐵 ∧ ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
53 51 52 bnj1198 ⊢ ( 𝜎 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
54 bnj252 ⊢ ( ( 𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ↔ ( 𝜎 ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
55 22 54 bitri ⊢ ( 𝜑 ↔ ( 𝜎 ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
56 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 bnj1445 ⊢ ( 𝜎 → ∀ 𝑑 𝜎 )
57 53 55 56 bnj1340 ⊢ ( 𝜎 → ∃ 𝑑 𝜑 )
58 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑧 ) )
59 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
60 bnj602 ⊢ ( 𝑥 = 𝑧 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑧 , 𝐴 , 𝑅 ) )
61 60 reseq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
62 59 61 opeq12d ⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
63 62 2 23 3eqtr4g ⊢ ( 𝑥 = 𝑧 → 𝑌 = 𝑋 )
64 63 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑋 ) )
65 58 64 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ↔ ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑋 ) ) )
66 22 bnj1254 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) )
67 20 simp3bi ⊢ ( 𝜌 → 𝑧 ∈ dom 𝑓 )
68 21 67 bnj769 ⊢ ( 𝜎 → 𝑧 ∈ dom 𝑓 )
69 22 68 bnj769 ⊢ ( 𝜑 → 𝑧 ∈ dom 𝑓 )
70 fndm ⊢ ( 𝑓 Fn 𝑑 → dom 𝑓 = 𝑑 )
71 22 70 bnj771 ⊢ ( 𝜑 → dom 𝑓 = 𝑑 )
72 69 71 eleqtrd ⊢ ( 𝜑 → 𝑧 ∈ 𝑑 )
73 65 66 72 rspcdva ⊢ ( 𝜑 → ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑋 ) )
74 16 bnj930 ⊢ ( 𝜒 → Fun 𝑄 )
75 17 74 bnj832 ⊢ ( 𝜃 → Fun 𝑄 )
76 19 75 bnj832 ⊢ ( 𝜁 → Fun 𝑄 )
77 20 76 bnj835 ⊢ ( 𝜌 → Fun 𝑄 )
78 21 77 bnj769 ⊢ ( 𝜎 → Fun 𝑄 )
79 22 78 bnj769 ⊢ ( 𝜑 → Fun 𝑄 )
80 20 simp2bi ⊢ ( 𝜌 → 𝑓 ∈ 𝐻 )
81 21 80 bnj769 ⊢ ( 𝜎 → 𝑓 ∈ 𝐻 )
82 22 81 bnj769 ⊢ ( 𝜑 → 𝑓 ∈ 𝐻 )
83 elssuni ⊢ ( 𝑓 ∈ 𝐻 → 𝑓 ⊆ ∪ 𝐻 )
84 83 10 sseqtrrdi ⊢ ( 𝑓 ∈ 𝐻 → 𝑓 ⊆ 𝑃 )
85 ssun3 ⊢ ( 𝑓 ⊆ 𝑃 → 𝑓 ⊆ ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } ) )
86 85 12 sseqtrrdi ⊢ ( 𝑓 ⊆ 𝑃 → 𝑓 ⊆ 𝑄 )
87 82 84 86 3syl ⊢ ( 𝜑 → 𝑓 ⊆ 𝑄 )
88 79 87 69 bnj1502 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑧 ) )
89 60 sseq1d ⊢ ( 𝑥 = 𝑧 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ↔ pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
90 1 bnj1517 ⊢ ( 𝑑 ∈ 𝐵 → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
91 22 90 bnj770 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
92 89 91 72 rspcdva ⊢ ( 𝜑 → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
93 92 71 sseqtrrd ⊢ ( 𝜑 → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ dom 𝑓 )
94 79 87 93 bnj1503 ⊢ ( 𝜑 → ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
95 94 opeq2d ⊢ ( 𝜑 → ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
96 95 13 23 3eqtr4g ⊢ ( 𝜑 → 𝑊 = 𝑋 )
97 96 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑊 ) = ( 𝐺 ‘ 𝑋 ) )
98 73 88 97 3eqtr4d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
99 57 98 bnj593 ⊢ ( 𝜎 → ∃ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1446 ⊢ ( ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) → ∀ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
101 99 100 bnj1397 ⊢ ( 𝜎 → ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
102 48 101 bnj593 ⊢ ( 𝜌 → ∃ 𝑦 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1447 ⊢ ( ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) → ∀ 𝑦 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
104 102 103 bnj1397 ⊢ ( 𝜌 → ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
105 36 104 bnj593 ⊢ ( 𝜁 → ∃ 𝑓 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
106 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1448 ⊢ ( ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) → ∀ 𝑓 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
107 105 106 bnj1397 ⊢ ( 𝜁 → ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )