Theorem tz7.48-1

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

	Ref	Expression
Hypothesis	tz7.48.1	⊢ 𝐹 Fn On
Assertion	tz7.48-1	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ran 𝐹 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		tz7.48.1	⊢ 𝐹 Fn On
2		vex	⊢ 𝑦 ∈ V
3	2	elrn2	⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
4		vex	⊢ 𝑥 ∈ V
5	4 2	opeldm	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹 )
6	1	fndmi	⊢ dom 𝐹 = On
7	5 6	eleqtrdi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑥 ∈ On )
8	7	ancri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ On ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
9		fnopfvb	⊢ ( ( 𝐹 Fn On ∧ 𝑥 ∈ On ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
10	1 9	mpan	⊢ ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
11	10	pm5.32i	⊢ ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ On ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
12	8 11	sylibr	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
13	12	eximi	⊢ ( ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
14	3 13	sylbi	⊢ ( 𝑦 ∈ ran 𝐹 → ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
15		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) )
16		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
17		rsp	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
18		eldifi	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
19		eleq1	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
20	18 19	syl5ibcom	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) )
21	20	imim2i	⊢ ( ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) )
22	21	impd	⊢ ( ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 ) )
23	17 22	syl	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 ) )
24	15 16 23	exlimd	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 ) )
25	14 24	syl5	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐴 ) )
26	25	ssrdv	⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ran 𝐹 ⊆ 𝐴 )