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 ⊢ F Fn On
Assertion tz7.48-2 ⊢ ∀ x ∈ On F ⁡ x ∈ A ∖ F x → Fun ⁡ F -1

Proof

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