This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ⊆ 𝐴 )