Metamath Proof Explorer

Theorem tz7.49c

Description: Corollary of Proposition 7.49 of TakeutiZaring p. 51. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 19-Jan-2013)

Ref Expression
Hypothesis tz7.49c.1 ⊢ 𝐹 Fn On
Assertion tz7.49c ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )

Proof

Step Hyp Ref Expression
1 tz7.49c.1 ⊢ 𝐹 Fn On
2 biid ⊢ ( ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) )
3 1 2 tz7.49 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∖ ( 𝐹 “ 𝑦 ) ) ≠ ∅ ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) )
4 3simpc ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∖ ( 𝐹 “ 𝑦 ) ) ≠ ∅ ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ( ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) )
5 onss ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
6 fnssres ⊢ ( ( 𝐹 Fn On ∧ 𝑥 ⊆ On ) → ( 𝐹 ↾ 𝑥 ) Fn 𝑥 )
7 1 5 6 sylancr ⊢ ( 𝑥 ∈ On → ( 𝐹 ↾ 𝑥 ) Fn 𝑥 )
8 df-ima ⊢ ( 𝐹 “ 𝑥 ) = ran ( 𝐹 ↾ 𝑥 )
9 8 eqeq1i ⊢ ( ( 𝐹 “ 𝑥 ) = 𝐴 ↔ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 )
10 9 biimpi ⊢ ( ( 𝐹 “ 𝑥 ) = 𝐴 → ran ( 𝐹 ↾ 𝑥 ) = 𝐴 )
11 7 10 anim12i ⊢ ( ( 𝑥 ∈ On ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ) → ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) )
12 11 anim1i ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ) ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ( ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) )
13 dff1o2 ⊢ ( ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ↔ ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) )
14 3anan32 ⊢ ( ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) ↔ ( ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) )
15 13 14 bitri ⊢ ( ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ↔ ( ( ( 𝐹 ↾ 𝑥 ) Fn 𝑥 ∧ ran ( 𝐹 ↾ 𝑥 ) = 𝐴 ) ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) )
16 12 15 sylibr ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ) ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )
17 16 expl ⊢ ( 𝑥 ∈ On → ( ( ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ) )
18 4 17 syl5 ⊢ ( 𝑥 ∈ On → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∖ ( 𝐹 “ 𝑦 ) ) ≠ ∅ ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 ) )
19 18 reximia ⊢ ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∖ ( 𝐹 “ 𝑦 ) ) ≠ ∅ ∧ ( 𝐹 “ 𝑥 ) = 𝐴 ∧ Fun ◡ ( 𝐹 ↾ 𝑥 ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )
20 3 19 syl ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ On ( ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐴 )