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

Metamath Proof Explorer

Theorem bnj1386

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

Ref Expression
Hypotheses bnj1386.1 ⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
bnj1386.2 ⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
bnj1386.3 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
bnj1386.4 ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
Assertion bnj1386 ( 𝜓 → Fun ∪ 𝐴 )

Proof

Step Hyp Ref Expression
1 bnj1386.1 ⊢ ( 𝜑 ↔ ∀ 𝑓 ∈ 𝐴 Fun 𝑓 )
2 bnj1386.2 ⊢ 𝐷 = ( dom 𝑓 ∩ dom 𝑔 )
3 bnj1386.3 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( 𝑓 ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 ) ) )
4 bnj1386.4 ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑓 𝑥 ∈ 𝐴 )
5 biid ⊢ ( ∀ ℎ ∈ 𝐴 Fun ℎ ↔ ∀ ℎ ∈ 𝐴 Fun ℎ )
6 eqid ⊢ ( dom ℎ ∩ dom 𝑔 ) = ( dom ℎ ∩ dom 𝑔 )
7 biid ⊢ ( ( ∀ ℎ ∈ 𝐴 Fun ℎ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ ( dom ℎ ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom ℎ ∩ dom 𝑔 ) ) ) ↔ ( ∀ ℎ ∈ 𝐴 Fun ℎ ∧ ∀ ℎ ∈ 𝐴 ∀ 𝑔 ∈ 𝐴 ( ℎ ↾ ( dom ℎ ∩ dom 𝑔 ) ) = ( 𝑔 ↾ ( dom ℎ ∩ dom 𝑔 ) ) ) )
8 1 2 3 4 5 6 7 bnj1385 ⊢ ( 𝜓 → Fun ∪ 𝐴 )