tz7.48-3

Description: Proposition 7.48(3) of TakeutiZaring p. 51. (Contributed by NM, 9-Feb-1997)

		Ref	Expression
	Hypothesis	tz7.48.1	$⊢ F Fn On$
	Assertion	tz7.48-3	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to \neg A \in V$

Step	Hyp	Ref	Expression
1		tz7.48.1	$⊢ F Fn On$
2	1	fndmi	$⊢ dom F = On$
3		onprc	$⊢ \neg On \in V$
4	2 3	eqneltri	$⊢ \neg dom F \in V$
5	1	tz7.48-2	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to Fun F^{-1}$
6		funrnex	$⊢ dom F^{-1} \in V \to (Fun F^{-1} \to ran F^{-1} \in V)$
7	6	com12	$⊢ Fun F^{-1} \to (dom F^{-1} \in V \to ran F^{-1} \in V)$
8		df-rn	$⊢ ran F = dom F^{-1}$
9	8	eleq1i	$⊢ ran F \in V \leftrightarrow dom F^{-1} \in V$
10		dfdm4	$⊢ dom F = ran F^{-1}$
11	10	eleq1i	$⊢ dom F \in V \leftrightarrow ran F^{-1} \in V$
12	7 9 11	3imtr4g	$⊢ Fun F^{-1} \to (ran F \in V \to dom F \in V)$
13	5 12	syl	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to (ran F \in V \to dom F \in V)$
14	4 13	mtoi	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to \neg ran F \in V$
15	1	tz7.48-1	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to ran F \subseteq A$
16		ssexg	$⊢ (ran F \subseteq A \land A \in V) \to ran F \in V$
17	16	ex	$⊢ ran F \subseteq A \to (A \in V \to ran F \in V)$
18	15 17	syl	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to (A \in V \to ran F \in V)$
19	14 18	mtod	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to \neg A \in V$

Metamath Proof Explorer