Metamath Proof Explorer


Theorem bnj1463

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

Proof

Step Hyp Ref Expression
1 bnj1463.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1463.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1463.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
4 bnj1463.4 ( 𝜏 ↔ ( 𝑓𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1463.5 𝐷 = { 𝑥𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1463.6 ( 𝜓 ↔ ( 𝑅 FrSe 𝐴𝐷 ≠ ∅ ) )
7 bnj1463.7 ( 𝜒 ↔ ( 𝜓𝑥𝐷 ∧ ∀ 𝑦𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1463.8 ( 𝜏′[ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1463.9 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1463.10 𝑃 = 𝐻
11 bnj1463.11 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12 bnj1463.12 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺𝑍 ) ⟩ } )
13 bnj1463.13 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
14 bnj1463.14 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
15 bnj1463.15 ( 𝜒𝑄 ∈ V )
16 bnj1463.16 ( 𝜒 → ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
17 bnj1463.17 ( 𝜒𝑄 Fn 𝐸 )
18 bnj1463.18 ( 𝜒𝐸𝐵 )
19 18 elexd ( 𝜒𝐸 ∈ V )
20 eleq1 ( 𝑑 = 𝐸 → ( 𝑑𝐵𝐸𝐵 ) )
21 fneq2 ( 𝑑 = 𝐸 → ( 𝑄 Fn 𝑑𝑄 Fn 𝐸 ) )
22 raleq ( 𝑑 = 𝐸 → ( ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ↔ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
23 21 22 anbi12d ( 𝑑 = 𝐸 → ( ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ↔ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
24 20 23 anbi12d ( 𝑑 = 𝐸 → ( ( 𝑑𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) ↔ ( 𝐸𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) ) )
25 1 bnj1317 ( 𝑤𝐵 → ∀ 𝑑 𝑤𝐵 )
26 25 nfcii 𝑑 𝐵
27 26 nfel2 𝑑 𝐸𝐵
28 1 2 3 4 5 6 7 8 9 10 11 12 bnj1467 ( 𝑤𝑄 → ∀ 𝑑 𝑤𝑄 )
29 28 nfcii 𝑑 𝑄
30 nfcv 𝑑 𝐸
31 29 30 nffn 𝑑 𝑄 Fn 𝐸
32 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1446 ( ( 𝑄𝑧 ) = ( 𝐺𝑊 ) → ∀ 𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
33 32 nf5i 𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 )
34 30 33 nfralw 𝑑𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 )
35 31 34 nfan 𝑑 ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
36 27 35 nfan 𝑑 ( 𝐸𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
37 36 nf5ri ( ( 𝐸𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) → ∀ 𝑑 ( 𝐸𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
38 18 17 16 jca32 ( 𝜒 → ( 𝐸𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧𝐸 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
39 24 37 38 bnj1465 ( ( 𝜒𝐸 ∈ V ) → ∃ 𝑑 ( 𝑑𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
40 19 39 mpdan ( 𝜒 → ∃ 𝑑 ( 𝑑𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
41 df-rex ( ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ↔ ∃ 𝑑 ( 𝑑𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
42 40 41 sylibr ( 𝜒 → ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
43 nfcv 𝑓 𝐵
44 1 2 3 4 5 6 7 8 9 10 11 12 bnj1466 ( 𝑤𝑄 → ∀ 𝑓 𝑤𝑄 )
45 44 nfcii 𝑓 𝑄
46 nfcv 𝑓 𝑑
47 45 46 nffn 𝑓 𝑄 Fn 𝑑
48 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1448 ( ( 𝑄𝑧 ) = ( 𝐺𝑊 ) → ∀ 𝑓 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
49 48 nf5i 𝑓 ( 𝑄𝑧 ) = ( 𝐺𝑊 )
50 46 49 nfralw 𝑓𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 )
51 47 50 nfan 𝑓 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
52 43 51 nfrex 𝑓𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) )
53 52 nf5ri ( ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) → ∀ 𝑓𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
54 29 nfeq2 𝑑 𝑓 = 𝑄
55 fneq1 ( 𝑓 = 𝑄 → ( 𝑓 Fn 𝑑𝑄 Fn 𝑑 ) )
56 fveq1 ( 𝑓 = 𝑄 → ( 𝑓𝑧 ) = ( 𝑄𝑧 ) )
57 reseq1 ( 𝑓 = 𝑄 → ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) = ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
58 57 opeq2d ( 𝑓 = 𝑄 → ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
59 58 13 eqtr4di ( 𝑓 = 𝑄 → ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ = 𝑊 )
60 59 fveq2d ( 𝑓 = 𝑄 → ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺𝑊 ) )
61 56 60 eqeq12d ( 𝑓 = 𝑄 → ( ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
62 61 ralbidv ( 𝑓 = 𝑄 → ( ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) )
63 55 62 anbi12d ( 𝑓 = 𝑄 → ( ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
64 54 63 rexbid ( 𝑓 = 𝑄 → ( ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
65 53 64 44 bnj1468 ( 𝑄 ∈ V → ( [ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
66 15 65 syl ( 𝜒 → ( [ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑄𝑧 ) = ( 𝐺𝑊 ) ) ) )
67 42 66 mpbird ( 𝜒[ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
68 fveq2 ( 𝑥 = 𝑧 → ( 𝑓𝑥 ) = ( 𝑓𝑧 ) )
69 id ( 𝑥 = 𝑧𝑥 = 𝑧 )
70 bnj602 ( 𝑥 = 𝑧 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑧 , 𝐴 , 𝑅 ) )
71 70 reseq2d ( 𝑥 = 𝑧 → ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
72 69 71 opeq12d ( 𝑥 = 𝑧 → ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
73 2 72 syl5eq ( 𝑥 = 𝑧𝑌 = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
74 73 fveq2d ( 𝑥 = 𝑧 → ( 𝐺𝑌 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) )
75 68 74 eqeq12d ( 𝑥 = 𝑧 → ( ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ↔ ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
76 75 cbvralvw ( ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ↔ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) )
77 76 anbi2i ( ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ↔ ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
78 77 rexbii ( ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ↔ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
79 78 sbcbii ( [ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ↔ [ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧𝑑 ( 𝑓𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
80 67 79 sylibr ( 𝜒[ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) )
81 3 bnj1454 ( 𝑄 ∈ V → ( 𝑄𝐶[ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ) )
82 15 81 syl ( 𝜒 → ( 𝑄𝐶[ 𝑄 / 𝑓 ]𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) ) )
83 80 82 mpbird ( 𝜒𝑄𝐶 )