isarep2

Description: Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature " [ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex . (Contributed by NM, 26-Oct-2006)

	Ref	Expression
Hypotheses	isarep2.1	⊢ 𝐴 ∈ V
	isarep2.2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( ( 𝜑 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑧 )
Assertion	isarep2	⊢ ∃ 𝑤 𝑤 = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isarep2.1	⊢ 𝐴 ∈ V
2		isarep2.2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ( ( 𝜑 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑧 )
3		resima	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) “ 𝐴 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 )
4		resopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
5	4	imaeq1i	⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) “ 𝐴 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } “ 𝐴 )
6	3 5	eqtr3i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } “ 𝐴 )
7		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
8	2	rspec	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( ( 𝜑 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑧 ) )
9		nfv	⊢ Ⅎ 𝑧 𝜑
10	9	mo3	⊢ ( ∃* 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝜑 ∧ [ 𝑧 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑧 ) )
11	8 10	sylibr	⊢ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 )
12		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
13	11 12	mpbir	⊢ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
14	7 13	mpgbir	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
15	1	funimaex	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } “ 𝐴 ) ∈ V )
16	14 15	ax-mp	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } “ 𝐴 ) ∈ V
17	6 16	eqeltri	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) ∈ V
18	17	isseti	⊢ ∃ 𝑤 𝑤 = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 )

Metamath Proof Explorer

Theorem isarep2

Proof