Step |
Hyp |
Ref |
Expression |
1 |
|
bnj548.1 |
⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) ) |
2 |
|
bnj548.2 |
⊢ 𝐵 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
3 |
|
bnj548.3 |
⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
4 |
|
bnj548.4 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑚 , 𝐶 〉 } ) |
5 |
|
bnj548.5 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → 𝐺 Fn 𝑛 ) |
6 |
5
|
bnj930 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → Fun 𝐺 ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → Fun 𝐺 ) |
8 |
1
|
simp1bi |
⊢ ( 𝜏 → 𝑓 Fn 𝑚 ) |
9 |
|
fndm |
⊢ ( 𝑓 Fn 𝑚 → dom 𝑓 = 𝑚 ) |
10 |
|
eleq2 |
⊢ ( dom 𝑓 = 𝑚 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑚 ) ) |
11 |
10
|
biimpar |
⊢ ( ( dom 𝑓 = 𝑚 ∧ 𝑖 ∈ 𝑚 ) → 𝑖 ∈ dom 𝑓 ) |
12 |
9 11
|
sylan |
⊢ ( ( 𝑓 Fn 𝑚 ∧ 𝑖 ∈ 𝑚 ) → 𝑖 ∈ dom 𝑓 ) |
13 |
8 12
|
sylan |
⊢ ( ( 𝜏 ∧ 𝑖 ∈ 𝑚 ) → 𝑖 ∈ dom 𝑓 ) |
14 |
13
|
3ad2antl2 |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → 𝑖 ∈ dom 𝑓 ) |
15 |
7 14
|
jca |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → ( Fun 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) ) |
16 |
4
|
bnj931 |
⊢ 𝑓 ⊆ 𝐺 |
17 |
15 16
|
jctil |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → ( 𝑓 ⊆ 𝐺 ∧ ( Fun 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) ) ) |
18 |
|
3anan12 |
⊢ ( ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) ↔ ( 𝑓 ⊆ 𝐺 ∧ ( Fun 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) ) ) |
19 |
17 18
|
sylibr |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) ) |
20 |
|
funssfv |
⊢ ( ( Fun 𝐺 ∧ 𝑓 ⊆ 𝐺 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
21 |
|
iuneq1 |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
22 |
21
|
eqcomd |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
23 |
22 2 3
|
3eqtr4g |
⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → 𝐵 = 𝐾 ) |
24 |
19 20 23
|
3syl |
⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) ∧ 𝑖 ∈ 𝑚 ) → 𝐵 = 𝐾 ) |