resf1ext2b

Description: Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025)

		Ref	Expression
	Assertion	resf1ext2b	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]) \leftrightarrow Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		fssres	$⊢ (F : A ⟶ B \land C \subseteq A) \to ({F ↾}_{C}) : C ⟶ B$
2	1	3adant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ({F ↾}_{C}) : C ⟶ B$
3		df-f1	$⊢ ({F ↾}_{C}) : C \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{C}) : C ⟶ B \land Fun {({F ↾}_{C})}^{-1})$
4		resf1extb	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B)$
5		df-f1	$⊢ ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B \land Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$
6	5	simprbi	$⊢ ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1}$
7	4 6	biimtrdi	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$
8	7	expd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (F (X) \notin F [C] \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1}))$
9	3 8	biimtrrid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C ⟶ B \land Fun {({F ↾}_{C})}^{-1}) \to (F (X) \notin F [C] \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1}))$
10	2 9	mpand	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (Fun {({F ↾}_{C})}^{-1} \to (F (X) \notin F [C] \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1}))$
11	10	impd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]) \to Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$
12		simp1	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to F : A ⟶ B$
13		simp3	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to C \subseteq A$
14		eldifi	$⊢ X \in (A ∖ C) \to X \in A$
15	14	snssd	$⊢ X \in (A ∖ C) \to \{X\} \subseteq A$
16	15	3ad2ant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to \{X\} \subseteq A$
17	13 16	unssd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to C \cup \{X\} \subseteq A$
18	12 17	fssresd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B$
19	3	simprbi	$⊢ ({F ↾}_{C}) : C \underset{1-1}{⟶} B \to Fun {({F ↾}_{C})}^{-1}$
20	19	anim1i	$⊢ (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \to (Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C])$
21	4 20	biimtrrdi	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \to (Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]))$
22	5 21	biimtrrid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B \land Fun {({F ↾}_{(C \cup \{X\})})}^{-1}) \to (Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]))$
23	18 22	mpand	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (Fun {({F ↾}_{(C \cup \{X\})})}^{-1} \to (Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]))$
24	11 23	impbid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((Fun {({F ↾}_{C})}^{-1} \land F (X) \notin F [C]) \leftrightarrow Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$

Metamath Proof Explorer

Theorem resf1ext2b

Proof