Metamath Proof Explorer


Theorem wfaxpr

Description: The class of well-founded sets models the Axiom of Pairing ax-pr . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Hypothesis wfax.1 𝑊 = ( 𝑅1 “ On )
Assertion wfaxpr 𝑥𝑊𝑦𝑊𝑧𝑊𝑤𝑊 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )

Proof

Step Hyp Ref Expression
1 wfax.1 𝑊 = ( 𝑅1 “ On )
2 prwf ( ( 𝑥 ( 𝑅1 “ On ) ∧ 𝑦 ( 𝑅1 “ On ) ) → { 𝑥 , 𝑦 } ∈ ( 𝑅1 “ On ) )
3 1 eleq2i ( 𝑥𝑊𝑥 ( 𝑅1 “ On ) )
4 1 eleq2i ( 𝑦𝑊𝑦 ( 𝑅1 “ On ) )
5 3 4 anbi12i ( ( 𝑥𝑊𝑦𝑊 ) ↔ ( 𝑥 ( 𝑅1 “ On ) ∧ 𝑦 ( 𝑅1 “ On ) ) )
6 1 eleq2i ( { 𝑥 , 𝑦 } ∈ 𝑊 ↔ { 𝑥 , 𝑦 } ∈ ( 𝑅1 “ On ) )
7 2 5 6 3imtr4i ( ( 𝑥𝑊𝑦𝑊 ) → { 𝑥 , 𝑦 } ∈ 𝑊 )
8 7 rgen2 𝑥𝑊𝑦𝑊 { 𝑥 , 𝑦 } ∈ 𝑊
9 prclaxpr ( ∀ 𝑥𝑊𝑦𝑊 { 𝑥 , 𝑦 } ∈ 𝑊 → ∀ 𝑥𝑊𝑦𝑊𝑧𝑊𝑤𝑊 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 ) )
10 8 9 ax-mp 𝑥𝑊𝑦𝑊𝑧𝑊𝑤𝑊 ( ( 𝑤 = 𝑥𝑤 = 𝑦 ) → 𝑤𝑧 )