tz7.48-2

Description: Proposition 7.48(2) of TakeutiZaring p. 51. (Contributed by NM, 9-Feb-1997) (Revised by David Abernethy, 5-May-2013)

		Ref	Expression
	Hypothesis	tz7.48.1	$⊢ F Fn On$
	Assertion	tz7.48-2	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to Fun F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		tz7.48.1	$⊢ F Fn On$
2		ssid	$⊢ On \subseteq On$
3		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
4	3	ancoms	$⊢ (y \in x \land x \in On) \to y \in On$
5	1	fndmi	$⊢ dom F = On$
6	5	eleq2i	$⊢ y \in dom F \leftrightarrow y \in On$
7		fnfun	$⊢ F Fn On \to Fun F$
8	1 7	ax-mp	$⊢ Fun F$
9		funfvima	$⊢ (Fun F \land y \in dom F) \to (y \in x \to F (y) \in F [x])$
10	8 9	mpan	$⊢ y \in dom F \to (y \in x \to F (y) \in F [x])$
11	10	impcom	$⊢ (y \in x \land y \in dom F) \to F (y) \in F [x]$
12		eleq1a	$⊢ F (y) \in F [x] \to (F (x) = F (y) \to F (x) \in F [x])$
13		eldifn	$⊢ F (x) \in (A ∖ F [x]) \to \neg F (x) \in F [x]$
14	12 13	nsyli	$⊢ F (y) \in F [x] \to (F (x) \in (A ∖ F [x]) \to \neg F (x) = F (y))$
15	11 14	syl	$⊢ (y \in x \land y \in dom F) \to (F (x) \in (A ∖ F [x]) \to \neg F (x) = F (y))$
16	6 15	sylan2br	$⊢ (y \in x \land y \in On) \to (F (x) \in (A ∖ F [x]) \to \neg F (x) = F (y))$
17	4 16	syldan	$⊢ (y \in x \land x \in On) \to (F (x) \in (A ∖ F [x]) \to \neg F (x) = F (y))$
18	17	expimpd	$⊢ y \in x \to ((x \in On \land F (x) \in (A ∖ F [x])) \to \neg F (x) = F (y))$
19	18	com12	$⊢ (x \in On \land F (x) \in (A ∖ F [x])) \to (y \in x \to \neg F (x) = F (y))$
20	19	ralrimiv	$⊢ (x \in On \land F (x) \in (A ∖ F [x])) \to \forall y \in x \neg F (x) = F (y)$
21	20	ralimiaa	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to \forall x \in On \forall y \in x \neg F (x) = F (y)$
22	1	tz7.48lem	$⊢ (On \subseteq On \land \forall x \in On \forall y \in x \neg F (x) = F (y)) \to Fun {({F ↾}_{On})}^{-1}$
23	2 21 22	sylancr	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to Fun {({F ↾}_{On})}^{-1}$
24		fnrel	$⊢ F Fn On \to Rel F$
25	1 24	ax-mp	$⊢ Rel F$
26	5	eqimssi	$⊢ dom F \subseteq On$
27		relssres	$⊢ (Rel F \land dom F \subseteq On) \to {F ↾}_{On} = F$
28	25 26 27	mp2an	$⊢ {F ↾}_{On} = F$
29	28	cnveqi	$⊢ {({F ↾}_{On})}^{-1} = F^{-1}$
30	29	funeqi	$⊢ Fun {({F ↾}_{On})}^{-1} \leftrightarrow Fun F^{-1}$
31	23 30	sylib	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to Fun F^{-1}$

Metamath Proof Explorer

Theorem tz7.48-2

Proof