Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1321.1 |
⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) } |
2 |
|
bnj1321.2 |
⊢ 𝑌 = 〈 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 |
3 |
|
bnj1321.3 |
⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) } |
4 |
|
bnj1321.4 |
⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ) |
5 |
|
simpr |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∃ 𝑓 𝜏 ) → ∃ 𝑓 𝜏 ) |
6 |
|
simp1 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑅 FrSe 𝐴 ) |
7 |
4
|
simplbi |
⊢ ( 𝜏 → 𝑓 ∈ 𝐶 ) |
8 |
7
|
3ad2ant2 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 ∈ 𝐶 ) |
9 |
|
nfab1 |
⊢ Ⅎ 𝑓 { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) } |
10 |
3 9
|
nfcxfr |
⊢ Ⅎ 𝑓 𝐶 |
11 |
10
|
nfcri |
⊢ Ⅎ 𝑓 𝑔 ∈ 𝐶 |
12 |
|
nfv |
⊢ Ⅎ 𝑓 dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) |
13 |
11 12
|
nfan |
⊢ Ⅎ 𝑓 ( 𝑔 ∈ 𝐶 ∧ dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
14 |
|
eleq1w |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ 𝐶 ↔ 𝑔 ∈ 𝐶 ) ) |
15 |
|
dmeq |
⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 ) |
16 |
15
|
eqeq1d |
⊢ ( 𝑓 = 𝑔 → ( dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ↔ dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ) |
17 |
14 16
|
anbi12d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑔 ∈ 𝐶 ∧ dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ) ) |
18 |
4 17
|
syl5bb |
⊢ ( 𝑓 = 𝑔 → ( 𝜏 ↔ ( 𝑔 ∈ 𝐶 ∧ dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ) ) |
19 |
13 18
|
sbiev |
⊢ ( [ 𝑔 / 𝑓 ] 𝜏 ↔ ( 𝑔 ∈ 𝐶 ∧ dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) ) |
20 |
19
|
simplbi |
⊢ ( [ 𝑔 / 𝑓 ] 𝜏 → 𝑔 ∈ 𝐶 ) |
21 |
20
|
3ad2ant3 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑔 ∈ 𝐶 ) |
22 |
|
eqid |
⊢ ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝑓 ∩ dom 𝑔 ) |
23 |
1 2 3 22
|
bnj1326 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑓 ∈ 𝐶 ∧ 𝑔 ∈ 𝐶 ) → ( 𝑓 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) ) |
24 |
6 8 21 23
|
syl3anc |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑓 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) ) |
25 |
4
|
simprbi |
⊢ ( 𝜏 → dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
26 |
25
|
3ad2ant2 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
27 |
19
|
simprbi |
⊢ ( [ 𝑔 / 𝑓 ] 𝜏 → dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
28 |
27
|
3ad2ant3 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → dom 𝑔 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
29 |
26 28
|
eqtr4d |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → dom 𝑓 = dom 𝑔 ) |
30 |
|
bnj1322 |
⊢ ( dom 𝑓 = dom 𝑔 → ( dom 𝑓 ∩ dom 𝑔 ) = dom 𝑓 ) |
31 |
30
|
reseq2d |
⊢ ( dom 𝑓 = dom 𝑔 → ( 𝑓 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑓 ↾ dom 𝑓 ) ) |
32 |
29 31
|
syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑓 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑓 ↾ dom 𝑓 ) ) |
33 |
|
releq |
⊢ ( 𝑧 = 𝑓 → ( Rel 𝑧 ↔ Rel 𝑓 ) ) |
34 |
1 2 3
|
bnj66 |
⊢ ( 𝑧 ∈ 𝐶 → Rel 𝑧 ) |
35 |
33 34
|
vtoclga |
⊢ ( 𝑓 ∈ 𝐶 → Rel 𝑓 ) |
36 |
|
resdm |
⊢ ( Rel 𝑓 → ( 𝑓 ↾ dom 𝑓 ) = 𝑓 ) |
37 |
8 35 36
|
3syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑓 ↾ dom 𝑓 ) = 𝑓 ) |
38 |
32 37
|
eqtrd |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑓 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = 𝑓 ) |
39 |
|
eqeq2 |
⊢ ( dom 𝑓 = dom 𝑔 → ( ( dom 𝑓 ∩ dom 𝑔 ) = dom 𝑓 ↔ ( dom 𝑓 ∩ dom 𝑔 ) = dom 𝑔 ) ) |
40 |
30 39
|
mpbid |
⊢ ( dom 𝑓 = dom 𝑔 → ( dom 𝑓 ∩ dom 𝑔 ) = dom 𝑔 ) |
41 |
40
|
reseq2d |
⊢ ( dom 𝑓 = dom 𝑔 → ( 𝑔 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑔 ↾ dom 𝑔 ) ) |
42 |
29 41
|
syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑔 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = ( 𝑔 ↾ dom 𝑔 ) ) |
43 |
1 2 3
|
bnj66 |
⊢ ( 𝑔 ∈ 𝐶 → Rel 𝑔 ) |
44 |
|
resdm |
⊢ ( Rel 𝑔 → ( 𝑔 ↾ dom 𝑔 ) = 𝑔 ) |
45 |
21 43 44
|
3syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑔 ↾ dom 𝑔 ) = 𝑔 ) |
46 |
42 45
|
eqtrd |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → ( 𝑔 ↾ ( dom 𝑓 ∩ dom 𝑔 ) ) = 𝑔 ) |
47 |
24 38 46
|
3eqtr3d |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 = 𝑔 ) |
48 |
47
|
3expib |
⊢ ( 𝑅 FrSe 𝐴 → ( ( 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 = 𝑔 ) ) |
49 |
48
|
alrimivv |
⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑓 ∀ 𝑔 ( ( 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 = 𝑔 ) ) |
50 |
49
|
adantr |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∃ 𝑓 𝜏 ) → ∀ 𝑓 ∀ 𝑔 ( ( 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 = 𝑔 ) ) |
51 |
|
nfv |
⊢ Ⅎ 𝑔 𝜏 |
52 |
51
|
eu2 |
⊢ ( ∃! 𝑓 𝜏 ↔ ( ∃ 𝑓 𝜏 ∧ ∀ 𝑓 ∀ 𝑔 ( ( 𝜏 ∧ [ 𝑔 / 𝑓 ] 𝜏 ) → 𝑓 = 𝑔 ) ) ) |
53 |
5 50 52
|
sylanbrc |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∃ 𝑓 𝜏 ) → ∃! 𝑓 𝜏 ) |