Metamath Proof Explorer

Theorem traxext

Description: A transitive class models the Axiom of Extensionality ax-ext . Lemma II.2.4(1) of Kunen2 p. 111. (Contributed by Eric Schmidt, 11-Sep-2025)

Ref Expression
Assertion traxext 
|- ( Tr M -> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. z e. M ( z e. x <-> z e. y ) <-> A. z ( z e. M -> ( z e. x <-> z e. y ) ) )
2 trel 
 |-  ( Tr M -> ( ( z e. x /\ x e. M ) -> z e. M ) )
3 2 ancomsd 
 |-  ( Tr M -> ( ( x e. M /\ z e. x ) -> z e. M ) )
4 3 expdimp 
 |-  ( ( Tr M /\ x e. M ) -> ( z e. x -> z e. M ) )
5 4 adantrr 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( z e. x -> z e. M ) )
6 5 adantr 
 |-  ( ( ( Tr M /\ ( x e. M /\ y e. M ) ) /\ ( z e. M -> ( z e. x <-> z e. y ) ) ) -> ( z e. x -> z e. M ) )
7 trel 
 |-  ( Tr M -> ( ( z e. y /\ y e. M ) -> z e. M ) )
8 7 ancomsd 
 |-  ( Tr M -> ( ( y e. M /\ z e. y ) -> z e. M ) )
9 8 expdimp 
 |-  ( ( Tr M /\ y e. M ) -> ( z e. y -> z e. M ) )
10 9 adantrl 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( z e. y -> z e. M ) )
11 10 adantr 
 |-  ( ( ( Tr M /\ ( x e. M /\ y e. M ) ) /\ ( z e. M -> ( z e. x <-> z e. y ) ) ) -> ( z e. y -> z e. M ) )
12 simpr 
 |-  ( ( ( Tr M /\ ( x e. M /\ y e. M ) ) /\ ( z e. M -> ( z e. x <-> z e. y ) ) ) -> ( z e. M -> ( z e. x <-> z e. y ) ) )
13 6 11 12 pm5.21ndd 
 |-  ( ( ( Tr M /\ ( x e. M /\ y e. M ) ) /\ ( z e. M -> ( z e. x <-> z e. y ) ) ) -> ( z e. x <-> z e. y ) )
14 13 ex 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( ( z e. M -> ( z e. x <-> z e. y ) ) -> ( z e. x <-> z e. y ) ) )
15 14 alimdv 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( A. z ( z e. M -> ( z e. x <-> z e. y ) ) -> A. z ( z e. x <-> z e. y ) ) )
16 1 15 biimtrid 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( A. z e. M ( z e. x <-> z e. y ) -> A. z ( z e. x <-> z e. y ) ) )
17 ax-ext 
 |-  ( A. z ( z e. x <-> z e. y ) -> x = y )
18 16 17 syl6 
 |-  ( ( Tr M /\ ( x e. M /\ y e. M ) ) -> ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) )
19 18 ralrimivva 
 |-  ( Tr M -> A. x e. M A. y e. M ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) )