| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1→𝐵) | 
| 2 |  | relcnv 6121 | . . . . . . 7
⊢ Rel ◡𝐴 | 
| 3 |  | cnvf1o 8137 | . . . . . . 7
⊢ (Rel
◡𝐴 → (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1-onto→◡◡𝐴) | 
| 4 |  | f1of1 6846 | . . . . . . 7
⊢ ((𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1-onto→◡◡𝐴 → (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→◡◡𝐴) | 
| 5 | 2, 3, 4 | mp2b 10 | . . . . . 6
⊢ (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→◡◡𝐴 | 
| 6 |  | simpl 482 | . . . . . . . 8
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → Rel 𝐴) | 
| 7 |  | dfrel2 6208 | . . . . . . . 8
⊢ (Rel
𝐴 ↔ ◡◡𝐴 = 𝐴) | 
| 8 | 6, 7 | sylib 218 | . . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → ◡◡𝐴 = 𝐴) | 
| 9 |  | f1eq3 6800 | . . . . . . 7
⊢ (◡◡𝐴 = 𝐴 → ((𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→◡◡𝐴 ↔ (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴)) | 
| 10 | 8, 9 | syl 17 | . . . . . 6
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → ((𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→◡◡𝐴 ↔ (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴)) | 
| 11 | 5, 10 | mpbii 233 | . . . . 5
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴) | 
| 12 |  | f1dm 6807 | . . . . . . . 8
⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) | 
| 13 | 1, 12 | syl 17 | . . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → dom 𝐹 = 𝐴) | 
| 14 | 13 | cnveqd 5885 | . . . . . 6
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → ◡dom 𝐹 = ◡𝐴) | 
| 15 |  | mpteq1 5234 | . . . . . 6
⊢ (◡dom 𝐹 = ◡𝐴 → (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) = (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥})) | 
| 16 |  | f1eq1 6798 | . . . . . 6
⊢ ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}) = (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}) → ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴 ↔ (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴)) | 
| 17 | 14, 15, 16 | 3syl 18 | . . . . 5
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → ((𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴 ↔ (𝑥 ∈ ◡𝐴 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴)) | 
| 18 | 11, 17 | mpbird 257 | . . . 4
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴) | 
| 19 |  | f1co 6814 | . . . 4
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}):◡𝐴–1-1→𝐴) → (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})):◡𝐴–1-1→𝐵) | 
| 20 | 1, 18, 19 | syl2anc 584 | . . 3
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})):◡𝐴–1-1→𝐵) | 
| 21 | 12 | releqd 5787 | . . . . 5
⊢ (𝐹:𝐴–1-1→𝐵 → (Rel dom 𝐹 ↔ Rel 𝐴)) | 
| 22 | 21 | biimparc 479 | . . . 4
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → Rel dom 𝐹) | 
| 23 |  | dftpos2 8269 | . . . 4
⊢ (Rel dom
𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | 
| 24 |  | f1eq1 6798 | . . . 4
⊢ (tpos
𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})) → (tpos 𝐹:◡𝐴–1-1→𝐵 ↔ (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})):◡𝐴–1-1→𝐵)) | 
| 25 | 22, 23, 24 | 3syl 18 | . . 3
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → (tpos 𝐹:◡𝐴–1-1→𝐵 ↔ (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})):◡𝐴–1-1→𝐵)) | 
| 26 | 20, 25 | mpbird 257 | . 2
⊢ ((Rel
𝐴 ∧ 𝐹:𝐴–1-1→𝐵) → tpos 𝐹:◡𝐴–1-1→𝐵) | 
| 27 | 26 | ex 412 | 1
⊢ (Rel
𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) |