Proof of Theorem preiman0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-rn 5696 | . . . . . 6
⊢ ran 𝐹 = dom ◡𝐹 | 
| 2 | 1 | ineq1i 4216 | . . . . 5
⊢ (ran
𝐹 ∩ (𝐴 ∩ ran 𝐹)) = (dom ◡𝐹 ∩ (𝐴 ∩ ran 𝐹)) | 
| 3 |  | dfss2 3969 | . . . . . . . . 9
⊢ (𝐴 ⊆ ran 𝐹 ↔ (𝐴 ∩ ran 𝐹) = 𝐴) | 
| 4 | 3 | biimpi 216 | . . . . . . . 8
⊢ (𝐴 ⊆ ran 𝐹 → (𝐴 ∩ ran 𝐹) = 𝐴) | 
| 5 | 4 | ineq2d 4220 | . . . . . . 7
⊢ (𝐴 ⊆ ran 𝐹 → (ran 𝐹 ∩ (𝐴 ∩ ran 𝐹)) = (ran 𝐹 ∩ 𝐴)) | 
| 6 |  | sseqin2 4223 | . . . . . . . 8
⊢ (𝐴 ⊆ ran 𝐹 ↔ (ran 𝐹 ∩ 𝐴) = 𝐴) | 
| 7 | 6 | biimpi 216 | . . . . . . 7
⊢ (𝐴 ⊆ ran 𝐹 → (ran 𝐹 ∩ 𝐴) = 𝐴) | 
| 8 | 5, 7 | eqtrd 2777 | . . . . . 6
⊢ (𝐴 ⊆ ran 𝐹 → (ran 𝐹 ∩ (𝐴 ∩ ran 𝐹)) = 𝐴) | 
| 9 | 8 | 3ad2ant2 1135 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝐴) = ∅) → (ran 𝐹 ∩ (𝐴 ∩ ran 𝐹)) = 𝐴) | 
| 10 |  | fimacnvinrn 7091 | . . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) | 
| 11 | 10 | eqeq1d 2739 | . . . . . . . 8
⊢ (Fun
𝐹 → ((◡𝐹 “ 𝐴) = ∅ ↔ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ∅)) | 
| 12 | 11 | biimpa 476 | . . . . . . 7
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝐴) = ∅) → (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ∅) | 
| 13 | 12 | 3adant2 1132 | . . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝐴) = ∅) → (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ∅) | 
| 14 |  | imadisj 6098 | . . . . . 6
⊢ ((◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ∅ ↔ (dom ◡𝐹 ∩ (𝐴 ∩ ran 𝐹)) = ∅) | 
| 15 | 13, 14 | sylib 218 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝐴) = ∅) → (dom ◡𝐹 ∩ (𝐴 ∩ ran 𝐹)) = ∅) | 
| 16 | 2, 9, 15 | 3eqtr3a 2801 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝐴) = ∅) → 𝐴 = ∅) | 
| 17 | 16 | 3expia 1122 | . . 3
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹) → ((◡𝐹 “ 𝐴) = ∅ → 𝐴 = ∅)) | 
| 18 | 17 | necon3d 2961 | . 2
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹) → (𝐴 ≠ ∅ → (◡𝐹 “ 𝐴) ≠ ∅)) | 
| 19 | 18 | 3impia 1118 | 1
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅) |