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

Metamath Proof Explorer

Theorem bnj1385

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1385.1 ⊢ φ ↔ ∀ f ∈ A Fun ⁡ f
bnj1385.2 ⊢ D = dom ⁡ f ∩ dom ⁡ g
bnj1385.3 ⊢ ψ ↔ φ ∧ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D
bnj1385.4 ⊢ x ∈ A → ∀ f x ∈ A
bnj1385.5 No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
bnj1385.6 ⊢ E = dom ⁡ h ∩ dom ⁡ g
bnj1385.7 No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
Assertion bnj1385 ⊢ ψ → Fun ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 bnj1385.1 ⊢ φ ↔ ∀ f ∈ A Fun ⁡ f
2 bnj1385.2 ⊢ D = dom ⁡ f ∩ dom ⁡ g
3 bnj1385.3 ⊢ ψ ↔ φ ∧ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D
4 bnj1385.4 ⊢ x ∈ A → ∀ f x ∈ A
5 bnj1385.5 Could not format ( ph' <-> A. h e. A Fun h ) : No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
6 bnj1385.6 ⊢ E = dom ⁡ h ∩ dom ⁡ g
7 bnj1385.7 Could not format ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) : No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
8 nfv ⊢ Ⅎ h f ∈ A → Fun ⁡ f
9 4 nfcii ⊢ Ⅎ _ f A
10 9 nfcri ⊢ Ⅎ f h ∈ A
11 nfv ⊢ Ⅎ f Fun ⁡ h
12 10 11 nfim ⊢ Ⅎ f h ∈ A → Fun ⁡ h
13 eleq1w ⊢ f = h → f ∈ A ↔ h ∈ A
14 funeq ⊢ f = h → Fun ⁡ f ↔ Fun ⁡ h
15 13 14 imbi12d ⊢ f = h → f ∈ A → Fun ⁡ f ↔ h ∈ A → Fun ⁡ h
16 8 12 15 cbvalv1 ⊢ ∀ f f ∈ A → Fun ⁡ f ↔ ∀ h h ∈ A → Fun ⁡ h
17 df-ral ⊢ ∀ f ∈ A Fun ⁡ f ↔ ∀ f f ∈ A → Fun ⁡ f
18 df-ral ⊢ ∀ h ∈ A Fun ⁡ h ↔ ∀ h h ∈ A → Fun ⁡ h
19 16 17 18 3bitr4i ⊢ ∀ f ∈ A Fun ⁡ f ↔ ∀ h ∈ A Fun ⁡ h
20 19 1 5 3bitr4i Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |-
21 nfv ⊢ Ⅎ h f ∈ A → ∀ g ∈ A f ↾ D = g ↾ D
22 nfv ⊢ Ⅎ f h ↾ E = g ↾ E
23 9 22 nfralw ⊢ Ⅎ f ∀ g ∈ A h ↾ E = g ↾ E
24 10 23 nfim ⊢ Ⅎ f h ∈ A → ∀ g ∈ A h ↾ E = g ↾ E
25 dmeq ⊢ f = h → dom ⁡ f = dom ⁡ h
26 25 ineq1d ⊢ f = h → dom ⁡ f ∩ dom ⁡ g = dom ⁡ h ∩ dom ⁡ g
27 26 2 6 3eqtr4g ⊢ f = h → D = E
28 27 reseq2d ⊢ f = h → f ↾ D = f ↾ E
29 reseq1 ⊢ f = h → f ↾ E = h ↾ E
30 28 29 eqtrd ⊢ f = h → f ↾ D = h ↾ E
31 27 reseq2d ⊢ f = h → g ↾ D = g ↾ E
32 30 31 eqeq12d ⊢ f = h → f ↾ D = g ↾ D ↔ h ↾ E = g ↾ E
33 32 ralbidv ⊢ f = h → ∀ g ∈ A f ↾ D = g ↾ D ↔ ∀ g ∈ A h ↾ E = g ↾ E
34 13 33 imbi12d ⊢ f = h → f ∈ A → ∀ g ∈ A f ↾ D = g ↾ D ↔ h ∈ A → ∀ g ∈ A h ↾ E = g ↾ E
35 21 24 34 cbvalv1 ⊢ ∀ f f ∈ A → ∀ g ∈ A f ↾ D = g ↾ D ↔ ∀ h h ∈ A → ∀ g ∈ A h ↾ E = g ↾ E
36 df-ral ⊢ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D ↔ ∀ f f ∈ A → ∀ g ∈ A f ↾ D = g ↾ D
37 df-ral ⊢ ∀ h ∈ A ∀ g ∈ A h ↾ E = g ↾ E ↔ ∀ h h ∈ A → ∀ g ∈ A h ↾ E = g ↾ E
38 35 36 37 3bitr4i ⊢ ∀ f ∈ A ∀ g ∈ A f ↾ D = g ↾ D ↔ ∀ h ∈ A ∀ g ∈ A h ↾ E = g ↾ E
39 20 38 anbi12i Could not format ( ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) : No typesetting found for |- ( ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
40 39 3 7 3bitr4i Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |-
41 5 6 7 bnj1383 Could not format ( ps' -> Fun U. A ) : No typesetting found for |- ( ps' -> Fun U. A ) with typecode |-
42 40 41 sylbi ⊢ ψ → Fun ⁡ ⋃ A