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

Metamath Proof Explorer

Theorem tz7.48-3

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

Ref Expression
Hypothesis tz7.48.1 ⊢ 𝐹 Fn On
Assertion tz7.48-3 ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 tz7.48.1 ⊢ 𝐹 Fn On
2 1 fndmi ⊢ dom 𝐹 = On
3 onprc ⊢ ¬ On ∈ V
4 2 3 eqneltri ⊢ ¬ dom 𝐹 ∈ V
5 1 tz7.48-2 ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → Fun ◡ 𝐹 )
6 funrnex ⊢ ( dom ◡ 𝐹 ∈ V → ( Fun ◡ 𝐹 → ran ◡ 𝐹 ∈ V ) )
7 6 com12 ⊢ ( Fun ◡ 𝐹 → ( dom ◡ 𝐹 ∈ V → ran ◡ 𝐹 ∈ V ) )
8 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
9 8 eleq1i ⊢ ( ran 𝐹 ∈ V ↔ dom ◡ 𝐹 ∈ V )
10 dfdm4 ⊢ dom 𝐹 = ran ◡ 𝐹
11 10 eleq1i ⊢ ( dom 𝐹 ∈ V ↔ ran ◡ 𝐹 ∈ V )
12 7 9 11 3imtr4g ⊢ ( Fun ◡ 𝐹 → ( ran 𝐹 ∈ V → dom 𝐹 ∈ V ) )
13 5 12 syl ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( ran 𝐹 ∈ V → dom 𝐹 ∈ V ) )
14 4 13 mtoi ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ ran 𝐹 ∈ V )
15 1 tz7.48-1 ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ran 𝐹 ⊆ 𝐴 )
16 ssexg ⊢ ( ( ran 𝐹 ⊆ 𝐴 ∧ 𝐴 ∈ V ) → ran 𝐹 ∈ V )
17 16 ex ⊢ ( ran 𝐹 ⊆ 𝐴 → ( 𝐴 ∈ V → ran 𝐹 ∈ V ) )
18 15 17 syl ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ( 𝐴 ∈ V → ran 𝐹 ∈ V ) )
19 14 18 mtod ⊢ ( ∀ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐴 ∖ ( 𝐹 “ 𝑥 ) ) → ¬ 𝐴 ∈ V )