tz7.48-1

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

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

Proof

Step	Hyp	Ref	Expression
1		tz7.48.1	$⊢ F Fn On$
2		vex	$⊢ y \in V$
3	2	elrn2	$⊢ y \in ran F \leftrightarrow \exists x ⟨x, y⟩ \in F$
4		vex	$⊢ x \in V$
5	4 2	opeldm	$⊢ ⟨x, y⟩ \in F \to x \in dom F$
6	1	fndmi	$⊢ dom F = On$
7	5 6	eleqtrdi	$⊢ ⟨x, y⟩ \in F \to x \in On$
8	7	ancri	$⊢ ⟨x, y⟩ \in F \to (x \in On \land ⟨x, y⟩ \in F)$
9		fnopfvb	$⊢ (F Fn On \land x \in On) \to (F (x) = y \leftrightarrow ⟨x, y⟩ \in F)$
10	1 9	mpan	$⊢ x \in On \to (F (x) = y \leftrightarrow ⟨x, y⟩ \in F)$
11	10	pm5.32i	$⊢ (x \in On \land F (x) = y) \leftrightarrow (x \in On \land ⟨x, y⟩ \in F)$
12	8 11	sylibr	$⊢ ⟨x, y⟩ \in F \to (x \in On \land F (x) = y)$
13	12	eximi	$⊢ \exists x ⟨x, y⟩ \in F \to \exists x (x \in On \land F (x) = y)$
14	3 13	sylbi	$⊢ y \in ran F \to \exists x (x \in On \land F (x) = y)$
15		nfra1	$⊢ Ⅎ x \forall x \in On F (x) \in (A ∖ F [x])$
16		nfv	$⊢ Ⅎ x y \in A$
17		rsp	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to (x \in On \to F (x) \in (A ∖ F [x]))$
18		eldifi	$⊢ F (x) \in (A ∖ F [x]) \to F (x) \in A$
19		eleq1	$⊢ F (x) = y \to (F (x) \in A \leftrightarrow y \in A)$
20	18 19	syl5ibcom	$⊢ F (x) \in (A ∖ F [x]) \to (F (x) = y \to y \in A)$
21	20	imim2i	$⊢ (x \in On \to F (x) \in (A ∖ F [x])) \to (x \in On \to (F (x) = y \to y \in A))$
22	21	impd	$⊢ (x \in On \to F (x) \in (A ∖ F [x])) \to ((x \in On \land F (x) = y) \to y \in A)$
23	17 22	syl	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to ((x \in On \land F (x) = y) \to y \in A)$
24	15 16 23	exlimd	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to (\exists x (x \in On \land F (x) = y) \to y \in A)$
25	14 24	syl5	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to (y \in ran F \to y \in A)$
26	25	ssrdv	$⊢ \forall x \in On F (x) \in (A ∖ F [x]) \to ran F \subseteq A$

Metamath Proof Explorer

Theorem tz7.48-1

Proof