Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1259.1 |
⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) } |
2 |
|
bnj1259.2 |
⊢ 𝑌 = 〈 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 |
3 |
|
bnj1259.3 |
⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) } |
4 |
|
bnj1259.4 |
⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ ) |
5 |
|
bnj1259.5 |
⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } |
6 |
|
bnj1259.6 |
⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) ) |
7 |
|
bnj1259.7 |
⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) ) |
8 |
|
abid |
⊢ ( ℎ ∈ { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) } ↔ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) ) |
9 |
8
|
bnj1238 |
⊢ ( ℎ ∈ { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) } → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 ) |
10 |
|
eqid |
⊢ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 = 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 |
11 |
|
eqid |
⊢ { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) } = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) } |
12 |
2 3 10 11
|
bnj1234 |
⊢ 𝐶 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) } |
13 |
9 12
|
eleq2s |
⊢ ( ℎ ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 ) |
14 |
6 13
|
bnj771 |
⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 ) |