Theorem funin 3558

Description: The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53.

Assertion

Ref	Expression
funin	⊢ (Fun F → Fun (F ∩ G))

Proof of Theorem funin

Step	Hyp	Ref	Expression
1		relin1 3257	. . 3 ⊢ (Rel F → Rel (F ∩ G))
2		moan 1420	. . . . 5 ⊢ (∃*y xFy → ∃*y(⟨x, y⟩ ∈ G ⋀ xFy))
3		ancom 435	. . . . . . 7 ⊢ ((⟨x, y⟩ ∈ G ⋀ xFy) ↔ (xFy ⋀ ⟨x, y⟩ ∈ G))
4		elin 2203	. . . . . . . 8 ⊢ (⟨x, y⟩ ∈ (F ∩ G) ↔ (⟨x, y⟩ ∈ F ⋀ ⟨x, y⟩ ∈ G))
5		df-br 2615	. . . . . . . 8 ⊢ (x(F ∩ G)y ↔ ⟨x, y⟩ ∈ (F ∩ G))
6		df-br 2615	. . . . . . . . 9 ⊢ (xFy ↔ ⟨x, y⟩ ∈ F)
7	6	anbi1i 481	. . . . . . . 8 ⊢ ((xFy ⋀ ⟨x, y⟩ ∈ G) ↔ (⟨x, y⟩ ∈ F ⋀ ⟨x, y⟩ ∈ G))
8	4, 5, 7	3bitr4 183	. . . . . . 7 ⊢ (x(F ∩ G)y ↔ (xFy ⋀ ⟨x, y⟩ ∈ G))
9	3, 8	bitr4 176	. . . . . 6 ⊢ ((⟨x, y⟩ ∈ G ⋀ xFy) ↔ x(F ∩ G)y)
10	9	mobii 1403	. . . . 5 ⊢ (∃*y(⟨x, y⟩ ∈ G ⋀ xFy) ↔ ∃*y x(F ∩ G)y)
11	2, 10	sylib 198	. . . 4 ⊢ (∃*y xFy → ∃*y x(F ∩ G)y)
12	11	19.20i 990	. . 3 ⊢ (∀x∃*y xFy → ∀x∃*y x(F ∩ G)y)
13	1, 12	anim12i 333	. 2 ⊢ ((Rel F ⋀ ∀x∃*y xFy) → (Rel (F ∩ G) ⋀ ∀x∃*y x(F ∩ G)y))
14		dffunmo 3523	. 2 ⊢ (Fun F ↔ (Rel F ⋀ ∀x∃*y xFy))
15		dffunmo 3523	. 2 ⊢ (Fun (F ∩ G) ↔ (Rel (F ∩ G) ⋀ ∀x∃*y x(F ∩ G)y))
16	13, 14, 15	3imtr4 219	1 ⊢ (Fun F → Fun (F ∩ G))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   ∈ wcel 956  ∃*wmo 1379   ∩ cin 2042  ⟨cop 2407   class class class wbr 2614  Rel wrel 3170  Fun wfun 3171

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615  df-opab 2662  df-id 2830  df-rel 3180  df-cnv 3181  df-co 3182  df-fun 3187

Copyright terms: Public domain