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

Metamath Proof Explorer

Theorem fvn0ssdmfun

Description: If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 . (Contributed by AV, 27-Jan-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion fvn0ssdmfun ( ∀ 𝑎 ∈ 𝐷 ( 𝐹 ‘ 𝑎 ) ≠ ∅ → ( 𝐷 ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 fvfundmfvn0 ⊢ ( ( 𝐹 ‘ 𝑎 ) ≠ ∅ → ( 𝑎 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑎 } ) ) )
2 1 ralimi ⊢ ( ∀ 𝑎 ∈ 𝐷 ( 𝐹 ‘ 𝑎 ) ≠ ∅ → ∀ 𝑎 ∈ 𝐷 ( 𝑎 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑎 } ) ) )
3 r19.26 ⊢ ( ∀ 𝑎 ∈ 𝐷 ( 𝑎 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑎 } ) ) ↔ ( ∀ 𝑎 ∈ 𝐷 𝑎 ∈ dom 𝐹 ∧ ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) ) )
4 eleq1w ⊢ ( 𝑎 = 𝑝 → ( 𝑎 ∈ dom 𝐹 ↔ 𝑝 ∈ dom 𝐹 ) )
5 4 rspccv ⊢ ( ∀ 𝑎 ∈ 𝐷 𝑎 ∈ dom 𝐹 → ( 𝑝 ∈ 𝐷 → 𝑝 ∈ dom 𝐹 ) )
6 5 ssrdv ⊢ ( ∀ 𝑎 ∈ 𝐷 𝑎 ∈ dom 𝐹 → 𝐷 ⊆ dom 𝐹 )
7 funrel ⊢ ( Fun ( 𝐹 ↾ { 𝑎 } ) → Rel ( 𝐹 ↾ { 𝑎 } ) )
8 7 ralimi ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → ∀ 𝑎 ∈ 𝐷 Rel ( 𝐹 ↾ { 𝑎 } ) )
9 reliun ⊢ ( Rel ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) ↔ ∀ 𝑎 ∈ 𝐷 Rel ( 𝐹 ↾ { 𝑎 } ) )
10 8 9 sylibr ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → Rel ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) )
11 sneq ⊢ ( 𝑎 = 𝑥 → { 𝑎 } = { 𝑥 } )
12 11 reseq2d ⊢ ( 𝑎 = 𝑥 → ( 𝐹 ↾ { 𝑎 } ) = ( 𝐹 ↾ { 𝑥 } ) )
13 12 funeqd ⊢ ( 𝑎 = 𝑥 → ( Fun ( 𝐹 ↾ { 𝑎 } ) ↔ Fun ( 𝐹 ↾ { 𝑥 } ) ) )
14 13 rspcva ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) ) → Fun ( 𝐹 ↾ { 𝑥 } ) )
15 dffun5 ⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) ↔ ( Rel ( 𝐹 ↾ { 𝑥 } ) ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) ) )
16 vex ⊢ 𝑥 ∈ V
17 16 elsnres ⊢ ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) ↔ ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
18 17 imbi1i ⊢ ( ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) ↔ ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
19 18 albii ⊢ ( ∀ 𝑧 ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
20 19 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
21 20 albii ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
22 equcom ⊢ ( 𝑎 = 𝑧 ↔ 𝑧 = 𝑎 )
23 opeq12 ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑎 ) → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
24 23 ex ⊢ ( 𝑤 = 𝑥 → ( 𝑧 = 𝑎 → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ) )
25 22 24 biimtrid ⊢ ( 𝑤 = 𝑥 → ( 𝑎 = 𝑧 → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ) )
26 25 adantr ⊢ ( ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( 𝑎 = 𝑧 → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ) )
27 26 impcom ⊢ ( ( 𝑎 = 𝑧 ∧ ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
28 opeq2 ⊢ ( 𝑧 = 𝑎 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
29 28 equcoms ⊢ ( 𝑎 = 𝑧 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ )
30 29 eleq1d ⊢ ( 𝑎 = 𝑧 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
31 30 biimpcd ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → ( 𝑎 = 𝑧 → ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
32 31 adantl ⊢ ( ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( 𝑎 = 𝑧 → ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
33 32 impcom ⊢ ( ( 𝑎 = 𝑧 ∧ ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) → ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 )
34 27 33 jca ⊢ ( ( 𝑎 = 𝑧 ∧ ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) → ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
35 34 ex ⊢ ( 𝑎 = 𝑧 → ( ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) ) )
36 35 spimevw ⊢ ( ( 𝑤 = 𝑥 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) )
37 36 ex ⊢ ( 𝑤 = 𝑥 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) ) )
38 37 imim1d ⊢ ( 𝑤 = 𝑥 → ( ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
39 38 alimdv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
40 39 eximdv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
41 40 spimvw ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑎 ( ⟨ 𝑤 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑎 ⟩ ∧ ⟨ 𝑥 , 𝑎 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) )
42 21 41 sylbi ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑤 , 𝑧 ⟩ ∈ ( 𝐹 ↾ { 𝑥 } ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) )
43 15 42 simplbiim ⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) )
44 14 43 syl ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) ) → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) )
45 44 expcom ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
46 impexp ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐷 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
47 46 albii ⊢ ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
48 47 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
49 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐷 → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
50 49 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐷 → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
51 19.37v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐷 → ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
52 48 50 51 3bitri ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑧 = 𝑦 ) ) )
53 45 52 sylibr ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
54 53 alrimiv ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
55 resiun2 ⊢ ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) = ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } )
56 55 eqcomi ⊢ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) = ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } )
57 56 eleq2i ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) )
58 iunid ⊢ ∪ 𝑎 ∈ 𝐷 { 𝑎 } = 𝐷
59 58 reseq2i ⊢ ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) = ( 𝐹 ↾ 𝐷 )
60 59 eleq2i ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ↾ 𝐷 ) )
61 vex ⊢ 𝑧 ∈ V
62 61 opelresi ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ↾ 𝐷 ) ↔ ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
63 57 60 62 3bitri ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) ↔ ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
64 63 imbi1i ⊢ ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
65 64 albii ⊢ ( ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
66 65 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
67 66 albii ⊢ ( ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ 𝐷 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑧 = 𝑦 ) )
68 54 67 sylibr ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) )
69 dffun5 ⊢ ( Fun ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) ↔ ( Rel ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) ∧ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) → 𝑧 = 𝑦 ) ) )
70 10 68 69 sylanbrc ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → Fun ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) )
71 58 eqcomi ⊢ 𝐷 = ∪ 𝑎 ∈ 𝐷 { 𝑎 }
72 71 reseq2i ⊢ ( 𝐹 ↾ 𝐷 ) = ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } )
73 72 funeqi ⊢ ( Fun ( 𝐹 ↾ 𝐷 ) ↔ Fun ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) )
74 55 funeqi ⊢ ( Fun ( 𝐹 ↾ ∪ 𝑎 ∈ 𝐷 { 𝑎 } ) ↔ Fun ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) )
75 73 74 bitri ⊢ ( Fun ( 𝐹 ↾ 𝐷 ) ↔ Fun ∪ 𝑎 ∈ 𝐷 ( 𝐹 ↾ { 𝑎 } ) )
76 70 75 sylibr ⊢ ( ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) → Fun ( 𝐹 ↾ 𝐷 ) )
77 6 76 anim12i ⊢ ( ( ∀ 𝑎 ∈ 𝐷 𝑎 ∈ dom 𝐹 ∧ ∀ 𝑎 ∈ 𝐷 Fun ( 𝐹 ↾ { 𝑎 } ) ) → ( 𝐷 ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ 𝐷 ) ) )
78 3 77 sylbi ⊢ ( ∀ 𝑎 ∈ 𝐷 ( 𝑎 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑎 } ) ) → ( 𝐷 ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ 𝐷 ) ) )
79 2 78 syl ⊢ ( ∀ 𝑎 ∈ 𝐷 ( 𝐹 ‘ 𝑎 ) ≠ ∅ → ( 𝐷 ⊆ dom 𝐹 ∧ Fun ( 𝐹 ↾ 𝐷 ) ) )