Description: Alternate proof for mof0 with stronger requirements on distinct variables. Uses mo4 . (Contributed by Zhi Wang, 19-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mof0ALT | ⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f00 | ⊢ ( 𝑓 : 𝐴 ⟶ ∅ ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) ) | |
| 2 | 1 | simplbi | ⊢ ( 𝑓 : 𝐴 ⟶ ∅ → 𝑓 = ∅ ) |
| 3 | f00 | ⊢ ( 𝑔 : 𝐴 ⟶ ∅ ↔ ( 𝑔 = ∅ ∧ 𝐴 = ∅ ) ) | |
| 4 | 3 | simplbi | ⊢ ( 𝑔 : 𝐴 ⟶ ∅ → 𝑔 = ∅ ) |
| 5 | eqtr3 | ⊢ ( ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) → 𝑓 = 𝑔 ) | |
| 6 | 2 4 5 | syl2an | ⊢ ( ( 𝑓 : 𝐴 ⟶ ∅ ∧ 𝑔 : 𝐴 ⟶ ∅ ) → 𝑓 = 𝑔 ) |
| 7 | 6 | gen2 | ⊢ ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 : 𝐴 ⟶ ∅ ∧ 𝑔 : 𝐴 ⟶ ∅ ) → 𝑓 = 𝑔 ) |
| 8 | feq1 | ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : 𝐴 ⟶ ∅ ↔ 𝑔 : 𝐴 ⟶ ∅ ) ) | |
| 9 | 8 | mo4 | ⊢ ( ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅ ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 : 𝐴 ⟶ ∅ ∧ 𝑔 : 𝐴 ⟶ ∅ ) → 𝑓 = 𝑔 ) ) |
| 10 | 7 9 | mpbir | ⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅ |