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 ⊢ F Fn On
Assertion tz7.48-3 ⊢ ∀ x ∈ On F ⁡ x ∈ A ∖ F x → ¬ A ∈ V

Proof

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