tz7.49c

Description: Corollary of Proposition 7.49 of TakeutiZaring p. 51. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 19-Jan-2013)

		Ref	Expression
	Hypothesis	tz7.49c.1	$⊢ F Fn On$
	Assertion	tz7.49c	$⊢ (A \in B \land \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))) \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		tz7.49c.1	$⊢ F Fn On$
2		biid	$⊢ \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])) \leftrightarrow \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
3	1 2	tz7.49	$⊢ (A \in B \land \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))) \to \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1})$
4		3simpc	$⊢ (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}) \to (F [x] = A \land Fun {({F ↾}_{x})}^{-1})$
5		onss	$⊢ x \in On \to x \subseteq On$
6		fnssres	$⊢ (F Fn On \land x \subseteq On) \to ({F ↾}_{x}) Fn x$
7	1 5 6	sylancr	$⊢ x \in On \to ({F ↾}_{x}) Fn x$
8		df-ima	$⊢ F [x] = ran ({F ↾}_{x})$
9	8	eqeq1i	$⊢ F [x] = A \leftrightarrow ran ({F ↾}_{x}) = A$
10	9	biimpi	$⊢ F [x] = A \to ran ({F ↾}_{x}) = A$
11	7 10	anim12i	$⊢ (x \in On \land F [x] = A) \to (({F ↾}_{x}) Fn x \land ran ({F ↾}_{x}) = A)$
12	11	anim1i	$⊢ ((x \in On \land F [x] = A) \land Fun {({F ↾}_{x})}^{-1}) \to ((({F ↾}_{x}) Fn x \land ran ({F ↾}_{x}) = A) \land Fun {({F ↾}_{x})}^{-1})$
13		dff1o2	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \leftrightarrow (({F ↾}_{x}) Fn x \land Fun {({F ↾}_{x})}^{-1} \land ran ({F ↾}_{x}) = A)$
14		3anan32	$⊢ (({F ↾}_{x}) Fn x \land Fun {({F ↾}_{x})}^{-1} \land ran ({F ↾}_{x}) = A) \leftrightarrow ((({F ↾}_{x}) Fn x \land ran ({F ↾}_{x}) = A) \land Fun {({F ↾}_{x})}^{-1})$
15	13 14	bitri	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \leftrightarrow ((({F ↾}_{x}) Fn x \land ran ({F ↾}_{x}) = A) \land Fun {({F ↾}_{x})}^{-1})$
16	12 15	sylibr	$⊢ ((x \in On \land F [x] = A) \land Fun {({F ↾}_{x})}^{-1}) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$
17	16	expl	$⊢ x \in On \to ((F [x] = A \land Fun {({F ↾}_{x})}^{-1}) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A)$
18	4 17	syl5	$⊢ x \in On \to ((\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}) \to ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A)$
19	18	reximia	$⊢ \exists x \in On (\forall y \in x A ∖ F [y] \neq \emptyset \land F [x] = A \land Fun {({F ↾}_{x})}^{-1}) \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$
20	3 19	syl	$⊢ (A \in B \land \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))) \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$

Metamath Proof Explorer

Theorem tz7.49c

Proof