| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . 2
⊢ ((𝑅 FrSe 𝐴 ∧ ∃𝑓𝜏) → ∃𝑓𝜏) | 
| 2 |  | simp1 1136 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑅 FrSe 𝐴) | 
| 3 |  | bnj1321.4 | . . . . . . . . 9
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) | 
| 4 | 3 | simplbi 497 | . . . . . . . 8
⊢ (𝜏 → 𝑓 ∈ 𝐶) | 
| 5 | 4 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 ∈ 𝐶) | 
| 6 |  | bnj1321.3 | . . . . . . . . . . . . 13
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} | 
| 7 |  | nfab1 2906 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑓{𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} | 
| 8 | 6, 7 | nfcxfr 2902 | . . . . . . . . . . . 12
⊢
Ⅎ𝑓𝐶 | 
| 9 | 8 | nfcri 2896 | . . . . . . . . . . 11
⊢
Ⅎ𝑓 𝑔 ∈ 𝐶 | 
| 10 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑓dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) | 
| 11 | 9, 10 | nfan 1898 | . . . . . . . . . 10
⊢
Ⅎ𝑓(𝑔 ∈ 𝐶 ∧ dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | 
| 12 |  | eleq1w 2823 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 ∈ 𝐶 ↔ 𝑔 ∈ 𝐶)) | 
| 13 |  | dmeq 5913 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔) | 
| 14 | 13 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) ↔ dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) | 
| 15 | 12, 14 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) ↔ (𝑔 ∈ 𝐶 ∧ dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))) | 
| 16 | 3, 15 | bitrid 283 | . . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝜏 ↔ (𝑔 ∈ 𝐶 ∧ dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))) | 
| 17 | 11, 16 | sbiev 2313 | . . . . . . . . 9
⊢ ([𝑔 / 𝑓]𝜏 ↔ (𝑔 ∈ 𝐶 ∧ dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) | 
| 18 | 17 | simplbi 497 | . . . . . . . 8
⊢ ([𝑔 / 𝑓]𝜏 → 𝑔 ∈ 𝐶) | 
| 19 | 18 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑔 ∈ 𝐶) | 
| 20 |  | bnj1321.1 | . . . . . . . 8
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} | 
| 21 |  | bnj1321.2 | . . . . . . . 8
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 | 
| 22 |  | eqid 2736 | . . . . . . . 8
⊢ (dom
𝑓 ∩ dom 𝑔) = (dom 𝑓 ∩ dom 𝑔) | 
| 23 | 20, 21, 6, 22 | bnj1326 35041 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑓 ∈ 𝐶 ∧ 𝑔 ∈ 𝐶) → (𝑓 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑔 ↾ (dom 𝑓 ∩ dom 𝑔))) | 
| 24 | 2, 5, 19, 23 | syl3anc 1372 | . . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑓 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑔 ↾ (dom 𝑓 ∩ dom 𝑔))) | 
| 25 | 3 | simprbi 496 | . . . . . . . . . 10
⊢ (𝜏 → dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | 
| 26 | 25 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | 
| 27 | 17 | simprbi 496 | . . . . . . . . . 10
⊢ ([𝑔 / 𝑓]𝜏 → dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | 
| 28 | 27 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → dom 𝑔 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) | 
| 29 | 26, 28 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → dom 𝑓 = dom 𝑔) | 
| 30 |  | bnj1322 34837 | . . . . . . . . 9
⊢ (dom
𝑓 = dom 𝑔 → (dom 𝑓 ∩ dom 𝑔) = dom 𝑓) | 
| 31 | 30 | reseq2d 5996 | . . . . . . . 8
⊢ (dom
𝑓 = dom 𝑔 → (𝑓 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑓 ↾ dom 𝑓)) | 
| 32 | 29, 31 | syl 17 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑓 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑓 ↾ dom 𝑓)) | 
| 33 |  | releq 5785 | . . . . . . . . 9
⊢ (𝑧 = 𝑓 → (Rel 𝑧 ↔ Rel 𝑓)) | 
| 34 | 20, 21, 6 | bnj66 34875 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 → Rel 𝑧) | 
| 35 | 33, 34 | vtoclga 3576 | . . . . . . . 8
⊢ (𝑓 ∈ 𝐶 → Rel 𝑓) | 
| 36 |  | resdm 6043 | . . . . . . . 8
⊢ (Rel
𝑓 → (𝑓 ↾ dom 𝑓) = 𝑓) | 
| 37 | 5, 35, 36 | 3syl 18 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑓 ↾ dom 𝑓) = 𝑓) | 
| 38 | 32, 37 | eqtrd 2776 | . . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑓 ↾ (dom 𝑓 ∩ dom 𝑔)) = 𝑓) | 
| 39 |  | eqeq2 2748 | . . . . . . . . . 10
⊢ (dom
𝑓 = dom 𝑔 → ((dom 𝑓 ∩ dom 𝑔) = dom 𝑓 ↔ (dom 𝑓 ∩ dom 𝑔) = dom 𝑔)) | 
| 40 | 30, 39 | mpbid 232 | . . . . . . . . 9
⊢ (dom
𝑓 = dom 𝑔 → (dom 𝑓 ∩ dom 𝑔) = dom 𝑔) | 
| 41 | 40 | reseq2d 5996 | . . . . . . . 8
⊢ (dom
𝑓 = dom 𝑔 → (𝑔 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑔 ↾ dom 𝑔)) | 
| 42 | 29, 41 | syl 17 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑔 ↾ (dom 𝑓 ∩ dom 𝑔)) = (𝑔 ↾ dom 𝑔)) | 
| 43 | 20, 21, 6 | bnj66 34875 | . . . . . . . 8
⊢ (𝑔 ∈ 𝐶 → Rel 𝑔) | 
| 44 |  | resdm 6043 | . . . . . . . 8
⊢ (Rel
𝑔 → (𝑔 ↾ dom 𝑔) = 𝑔) | 
| 45 | 19, 43, 44 | 3syl 18 | . . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑔 ↾ dom 𝑔) = 𝑔) | 
| 46 | 42, 45 | eqtrd 2776 | . . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → (𝑔 ↾ (dom 𝑓 ∩ dom 𝑔)) = 𝑔) | 
| 47 | 24, 38, 46 | 3eqtr3d 2784 | . . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 = 𝑔) | 
| 48 | 47 | 3expib 1122 | . . . 4
⊢ (𝑅 FrSe 𝐴 → ((𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 = 𝑔)) | 
| 49 | 48 | alrimivv 1927 | . . 3
⊢ (𝑅 FrSe 𝐴 → ∀𝑓∀𝑔((𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 = 𝑔)) | 
| 50 | 49 | adantr 480 | . 2
⊢ ((𝑅 FrSe 𝐴 ∧ ∃𝑓𝜏) → ∀𝑓∀𝑔((𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 = 𝑔)) | 
| 51 |  | nfv 1913 | . . 3
⊢
Ⅎ𝑔𝜏 | 
| 52 | 51 | eu2 2608 | . 2
⊢
(∃!𝑓𝜏 ↔ (∃𝑓𝜏 ∧ ∀𝑓∀𝑔((𝜏 ∧ [𝑔 / 𝑓]𝜏) → 𝑓 = 𝑔))) | 
| 53 | 1, 50, 52 | sylanbrc 583 | 1
⊢ ((𝑅 FrSe 𝐴 ∧ ∃𝑓𝜏) → ∃!𝑓𝜏) |