Metamath Proof Explorer

Theorem tz7.48-2

Description: Proposition 7.48(2) of TakeutiZaring p. 51. (Contributed by NM, 9-Feb-1997) (Revised by David Abernethy, 5-May-2013)

Ref Expression
Hypothesis tz7.48.1 ⊢ 𝐹 Fn On
Assertion tz7.48-2 ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → Fun ◡ 𝐹 )

Proof

Step Hyp Ref Expression
1 tz7.48.1 ⊢ 𝐹 Fn On
2 ssid ⊢ On ⊆ On
3 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
4 3 ancoms ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ On ) → 𝑦 ∈ On )
5 1 fndmi ⊢ dom 𝐹 = On
6 5 eleq2i ⊢ ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ On )
7 fnfun ⊢ ( 𝐹 Fn On → Fun 𝐹 )
8 1 7 ax-mp ⊢ Fun 𝐹
9 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
10 8 9 mpan ⊢ ( 𝑦 ∈ dom 𝐹 → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
11 10 impcom ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) )
12 eleq1a ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝑥 ) ) )
13 eldifn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝑥 ) )
14 12 13 nsyli ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
15 11 14 syl ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
16 6 15 sylan2br ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ On ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
17 4 16 syldan ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ On ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
18 17 expimpd ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
19 18 com12 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
20 19 ralrimiv ⊢ ( ( 𝑥 ∈ On ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
21 20 ralimiaa ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
22 1 tz7.48lem ⊢ ( ( On ⊆ On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ On ) )
23 2 21 22 sylancr ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → Fun ◡ ( 𝐹 ↾ On ) )
24 fnrel ⊢ ( 𝐹 Fn On → Rel 𝐹 )
25 1 24 ax-mp ⊢ Rel 𝐹
26 5 eqimssi ⊢ dom 𝐹 ⊆ On
27 relssres ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ On ) → ( 𝐹 ↾ On ) = 𝐹 )
28 25 26 27 mp2an ⊢ ( 𝐹 ↾ On ) = 𝐹
29 28 cnveqi ⊢ ◡ ( 𝐹 ↾ On ) = ◡ 𝐹
30 29 funeqi ⊢ ( Fun ◡ ( 𝐹 ↾ On ) ↔ Fun ◡ 𝐹 )
31 23 30 sylib ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → Fun ◡ 𝐹 )