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	⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
	bnj1385.2	⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
	bnj1385.3	⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
	bnj1385.4	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
	bnj1385.5	⊢ ( 𝜑′ ↔ ∀ ℎ ∈ 𝐴 Fun ℎ )
	bnj1385.6	⊢ 𝐸 = ( dom ℎ ∩ dom 𝑔 )
	bnj1385.7	⊢ ( 𝜓′ ↔ ( 𝜑′ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
Assertion	bnj1385	⊢ ( 𝜓 → Fun ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj1385.1	⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
2		bnj1385.2	⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
3		bnj1385.3	⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
4		bnj1385.4	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
5		bnj1385.5	⊢ ( 𝜑′ ↔ ∀ ℎ ∈ 𝐴 Fun ℎ )
6		bnj1385.6	⊢ 𝐸 = ( dom ℎ ∩ dom 𝑔 )
7		bnj1385.7	⊢ ( 𝜓′ ↔ ( 𝜑′ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
8		nfv	⊢ Ⅎ ℎ ( 𝑓 ∈ 𝐴 → Fun 𝑓 )
9	4	nfcii	⊢ Ⅎ 𝑓 𝐴
10	9	nfcri	⊢ Ⅎ 𝑓 ℎ ∈ 𝐴
11		nfv	⊢ Ⅎ 𝑓 Fun ℎ
12	10 11	nfim	⊢ Ⅎ 𝑓 ( ℎ ∈ 𝐴 → Fun ℎ )
13		eleq1w	⊢ ( 𝑓 = ℎ → ( 𝑓 ∈ 𝐴 ↔ ℎ ∈ 𝐴 ) )
14		funeq	⊢ ( 𝑓 = ℎ → ( Fun 𝑓 ↔ Fun ℎ ) )
15	13 14	imbi12d	⊢ ( 𝑓 = ℎ → ( ( 𝑓 ∈ 𝐴 → Fun 𝑓 ) ↔ ( ℎ ∈ 𝐴 → Fun ℎ ) ) )
16	8 12 15	cbvalv1	⊢ ( ∀ 𝑓 ( 𝑓 ∈ 𝐴 → Fun 𝑓 ) ↔ ∀ ℎ ( ℎ ∈ 𝐴 → Fun ℎ ) )
17		df-ral	⊢ ( ∀ 𝑓 ∈ 𝐴 Fun 𝑓 ↔ ∀ 𝑓 ( 𝑓 ∈ 𝐴 → Fun 𝑓 ) )
18		df-ral	⊢ ( ∀ ℎ ∈ 𝐴 Fun ℎ ↔ ∀ ℎ ( ℎ ∈ 𝐴 → Fun ℎ ) )
19	16 17 18	3bitr4i	⊢ ( ∀ 𝑓 ∈ 𝐴 Fun 𝑓 ↔ ∀ ℎ ∈ 𝐴 Fun ℎ )
20	19 1 5	3bitr4i	⊢ ( 𝜑 ↔ 𝜑′ )
21		nfv	⊢ Ⅎ ℎ ( 𝑓 ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) )
22		nfv	⊢ Ⅎ 𝑓 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 )
23	9 22	nfralw	⊢ Ⅎ 𝑓 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 )
24	10 23	nfim	⊢ Ⅎ 𝑓 ( ℎ ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) )
25		dmeq	⊢ ( 𝑓 = ℎ → dom 𝑓 = dom ℎ )
26	25	ineq1d	⊢ ( 𝑓 = ℎ → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom ℎ ∩ dom 𝑔 ) )
27	26 2 6	3eqtr4g	⊢ ( 𝑓 = ℎ → 𝐷 = 𝐸 )
28	27	reseq2d	⊢ ( 𝑓 = ℎ → ( 𝑓 ↾ 𝐷 ) = ( 𝑓 ↾ 𝐸 ) )
29		reseq1	⊢ ( 𝑓 = ℎ → ( 𝑓 ↾ 𝐸 ) = ( ℎ ↾ 𝐸 ) )
30	28 29	eqtrd	⊢ ( 𝑓 = ℎ → ( 𝑓 ↾ 𝐷 ) = ( ℎ ↾ 𝐸 ) )
31	27	reseq2d	⊢ ( 𝑓 = ℎ → ( 𝑔 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐸 ) )
32	30 31	eqeq12d	⊢ ( 𝑓 = ℎ → ( ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ↔ ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
33	32	ralbidv	⊢ ( 𝑓 = ℎ → ( ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ↔ ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
34	13 33	imbi12d	⊢ ( 𝑓 = ℎ → ( ( 𝑓 ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) ↔ ( ℎ ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) ) )
35	21 24 34	cbvalv1	⊢ ( ∀ 𝑓 ( 𝑓 ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) ↔ ∀ ℎ ( ℎ ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
36		df-ral	⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ↔ ∀ 𝑓 ( 𝑓 ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
37		df-ral	⊢ ( ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ↔ ∀ ℎ ( ℎ ∈ 𝐴 → ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
38	35 36 37	3bitr4i	⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ↔ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) )
39	20 38	anbi12i	⊢ ( ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) ↔ ( 𝜑′ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ 𝐸 ) = ( 𝑔 ↾ 𝐸 ) ) )
40	39 3 7	3bitr4i	⊢ ( 𝜓 ↔ 𝜓′ )
41	5 6 7	bnj1383	⊢ ( 𝜓′ → Fun ∪ 𝐴 )
42	40 41	sylbi	⊢ ( 𝜓 → Fun ∪ 𝐴 )