Theorem tz7.48-3

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

	Ref	Expression
Hypothesis	tz7.48.1	⊢ 𝐹 Fn On
Assertion	tz7.48-3	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		tz7.48.1	⊢ 𝐹 Fn On
2	1	fndmi	⊢ dom 𝐹 = On
3		onprc	⊢ ¬ On ∈ V
4	2 3	eqneltri	⊢ ¬ dom 𝐹 ∈ V
5	1	tz7.48-2	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → Fun ◡ 𝐹 )
6		funrnex	⊢ ( dom ◡ 𝐹 ∈ V → ( Fun ◡ 𝐹 → ran ◡ 𝐹 ∈ V ) )
7	6	com12	⊢ ( Fun ◡ 𝐹 → ( dom ◡ 𝐹 ∈ V → ran ◡ 𝐹 ∈ V ) )
8		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
9	8	eleq1i	⊢ ( ran 𝐹 ∈ V ↔ dom ◡ 𝐹 ∈ V )
10		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
11	10	eleq1i	⊢ ( dom 𝐹 ∈ V ↔ ran ◡ 𝐹 ∈ V )
12	7 9 11	3imtr4g	⊢ ( Fun ◡ 𝐹 → ( ran 𝐹 ∈ V → dom 𝐹 ∈ V ) )
13	5 12	syl	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ran 𝐹 ∈ V → dom 𝐹 ∈ V ) )
14	4 13	mtoi	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ran 𝐹 ∈ V )
15	1	tz7.48-1	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ran 𝐹 ⊆ 𝐴 )
16		ssexg	⊢ ( ( ran 𝐹 ⊆ 𝐴 ∧ 𝐴 ∈ V ) → ran 𝐹 ∈ V )
17	16	ex	⊢ ( ran 𝐹 ⊆ 𝐴 → ( 𝐴 ∈ V → ran 𝐹 ∈ V ) )
18	15 17	syl	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝐴 ∈ V → ran 𝐹 ∈ V ) )
19	14 18	mtod	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ 𝐴 ∈ V )