Metamath Proof Explorer

Theorem axtcond

Description: A version of the Axiom of Transitive Containment with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Matthew House, 6-Apr-2026) (New usage is discouraged.)

Ref Expression
Assertion axtcond 
|- E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) )

Proof

Step Hyp Ref Expression
1 axtco2 
 |-  E. w A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) )
2 nfnae 
 |-  F/ y -. A. x x = y
3 nfnae 
 |-  F/ y -. A. x x = z
4 nfnae 
 |-  F/ y -. A. y y = z
5 2 3 4 nf3an 
 |-  F/ y ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z )
6 nfv 
 |-  F/ y A. v ( ( v = t \/ v e. w ) -> A. t ( t e. v -> t e. w ) )
7 equequ2 
 |-  ( t = x -> ( v = t <-> v = x ) )
8 7 orbi1d 
 |-  ( t = x -> ( ( v = t \/ v e. w ) <-> ( v = x \/ v e. w ) ) )
9 elequ1 
 |-  ( t = x -> ( t e. v <-> x e. v ) )
10 elequ1 
 |-  ( t = x -> ( t e. w <-> x e. w ) )
11 9 10 imbi12d 
 |-  ( t = x -> ( ( t e. v -> t e. w ) <-> ( x e. v -> x e. w ) ) )
12 11 cbvalvw 
 |-  ( A. t ( t e. v -> t e. w ) <-> A. x ( x e. v -> x e. w ) )
13 12 a1i 
 |-  ( t = x -> ( A. t ( t e. v -> t e. w ) <-> A. x ( x e. v -> x e. w ) ) )
14 8 13 imbi12d 
 |-  ( t = x -> ( ( ( v = t \/ v e. w ) -> A. t ( t e. v -> t e. w ) ) <-> ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) ) )
15 14 albidv 
 |-  ( t = x -> ( A. v ( ( v = t \/ v e. w ) -> A. t ( t e. v -> t e. w ) ) <-> A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) ) )
16 6 15 dvelimnf 
 |-  ( -. A. y y = x -> F/ y A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
17 16 naecoms 
 |-  ( -. A. x x = y -> F/ y A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
18 17 3ad2ant1 
 |-  ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) -> F/ y A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
19 nfnae 
 |-  F/ z -. A. x x = y
20 nfnae 
 |-  F/ z -. A. x x = z
21 nfnae 
 |-  F/ z -. A. y y = z
22 19 20 21 nf3an 
 |-  F/ z ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z )
23 nfeqf2 
 |-  ( -. A. z z = y -> F/ z w = y )
24 23 naecoms 
 |-  ( -. A. y y = z -> F/ z w = y )
25 24 3ad2ant3 
 |-  ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) -> F/ z w = y )
26 22 25 nfan1 
 |-  F/ z ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) /\ w = y )
27 simpl2 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) /\ w = y ) -> -. A. x x = z )
28 nfv 
 |-  F/ z ( ( v = t \/ v e. w ) -> A. t ( t e. v -> t e. w ) )
29 28 14 dvelimnf 
 |-  ( -. A. z z = x -> F/ z ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
30 29 naecoms 
 |-  ( -. A. x x = z -> F/ z ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
31 27 30 syl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) /\ w = y ) -> F/ z ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) )
32 equequ1 
 |-  ( v = z -> ( v = x <-> z = x ) )
33 32 adantl 
 |-  ( ( w = y /\ v = z ) -> ( v = x <-> z = x ) )
34 elequ12 
 |-  ( ( v = z /\ w = y ) -> ( v e. w <-> z e. y ) )
35 34 ancoms 
 |-  ( ( w = y /\ v = z ) -> ( v e. w <-> z e. y ) )
36 33 35 orbi12d 
 |-  ( ( w = y /\ v = z ) -> ( ( v = x \/ v e. w ) <-> ( z = x \/ z e. y ) ) )
37 36 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ ( w = y /\ v = z ) ) -> ( ( v = x \/ v e. w ) <-> ( z = x \/ z e. y ) ) )
38 nfnae 
 |-  F/ x -. A. x x = y
39 nfnae 
 |-  F/ x -. A. x x = z
40 38 39 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
41 nfeqf2 
 |-  ( -. A. x x = y -> F/ x w = y )
42 41 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x w = y )
43 nfeqf2 
 |-  ( -. A. x x = z -> F/ x v = z )
44 43 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x v = z )
45 42 44 nfand 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( w = y /\ v = z ) )
46 40 45 nfan1 
 |-  F/ x ( ( -. A. x x = y /\ -. A. x x = z ) /\ ( w = y /\ v = z ) )
47 elequ2 
 |-  ( v = z -> ( x e. v <-> x e. z ) )
48 47 adantl 
 |-  ( ( w = y /\ v = z ) -> ( x e. v <-> x e. z ) )
49 elequ2 
 |-  ( w = y -> ( x e. w <-> x e. y ) )
50 49 adantr 
 |-  ( ( w = y /\ v = z ) -> ( x e. w <-> x e. y ) )
51 48 50 imbi12d 
 |-  ( ( w = y /\ v = z ) -> ( ( x e. v -> x e. w ) <-> ( x e. z -> x e. y ) ) )
52 51 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ ( w = y /\ v = z ) ) -> ( ( x e. v -> x e. w ) <-> ( x e. z -> x e. y ) ) )
53 46 52 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ ( w = y /\ v = z ) ) -> ( A. x ( x e. v -> x e. w ) <-> A. x ( x e. z -> x e. y ) ) )
54 37 53 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ ( w = y /\ v = z ) ) -> ( ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
55 54 expr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = y ) -> ( v = z -> ( ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) ) )
56 55 3adantl3 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) /\ w = y ) -> ( v = z -> ( ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) ) )
57 26 31 56 cbvaldw 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) /\ w = y ) -> ( A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
58 57 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) -> ( w = y -> ( A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) ) )
59 5 18 58 cbvexdw 
 |-  ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) -> ( E. w A. v ( ( v = x \/ v e. w ) -> A. x ( x e. v -> x e. w ) ) <-> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
60 1 59 mpbii 
 |-  ( ( -. A. x x = y /\ -. A. x x = z /\ -. A. y y = z ) -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
61 60 3exp 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> ( -. A. y y = z -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) ) )
62 nfae 
 |-  F/ z A. y y = z
63 nfae 
 |-  F/ x A. y y = z
64 elequ2 
 |-  ( y = z -> ( x e. y <-> x e. z ) )
65 64 sps 
 |-  ( A. y y = z -> ( x e. y <-> x e. z ) )
66 65 biimprd 
 |-  ( A. y y = z -> ( x e. z -> x e. y ) )
67 63 66 alrimi 
 |-  ( A. y y = z -> A. x ( x e. z -> x e. y ) )
68 67 a1d 
 |-  ( A. y y = z -> ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
69 62 68 alrimi 
 |-  ( A. y y = z -> A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
70 69 19.8ad 
 |-  ( A. y y = z -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
71 70 a1i 
 |-  ( A. x x = y -> ( A. y y = z -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
72 ax-nul 
 |-  E. y A. u -. u e. y
73 nfv 
 |-  F/ z A. u -. u e. t
74 elequ2 
 |-  ( t = y -> ( u e. t <-> u e. y ) )
75 74 notbid 
 |-  ( t = y -> ( -. u e. t <-> -. u e. y ) )
76 75 albidv 
 |-  ( t = y -> ( A. u -. u e. t <-> A. u -. u e. y ) )
77 73 76 dvelimnf 
 |-  ( -. A. z z = y -> F/ z A. u -. u e. y )
78 77 naecoms 
 |-  ( -. A. y y = z -> F/ z A. u -. u e. y )
79 elequ2 
 |-  ( z = y -> ( u e. z <-> u e. y ) )
80 79 notbid 
 |-  ( z = y -> ( -. u e. z <-> -. u e. y ) )
81 80 albidv 
 |-  ( z = y -> ( A. u -. u e. z <-> A. u -. u e. y ) )
82 81 biimprcd 
 |-  ( A. u -. u e. y -> ( z = y -> A. u -. u e. z ) )
83 elirrv 
 |-  -. x e. x
84 elequ2 
 |-  ( x = z -> ( x e. x <-> x e. z ) )
85 83 84 mtbii 
 |-  ( x = z -> -. x e. z )
86 85 pm2.21d 
 |-  ( x = z -> ( x e. z -> x e. y ) )
87 86 alimi 
 |-  ( A. x x = z -> A. x ( x e. z -> x e. y ) )
88 87 a1d 
 |-  ( A. x x = z -> ( A. u -. u e. z -> A. x ( x e. z -> x e. y ) ) )
89 nfv 
 |-  F/ x A. u -. u e. t
90 elequ2 
 |-  ( t = z -> ( u e. t <-> u e. z ) )
91 90 notbid 
 |-  ( t = z -> ( -. u e. t <-> -. u e. z ) )
92 91 albidv 
 |-  ( t = z -> ( A. u -. u e. t <-> A. u -. u e. z ) )
93 89 92 dvelimnf 
 |-  ( -. A. x x = z -> F/ x A. u -. u e. z )
94 elequ1 
 |-  ( u = x -> ( u e. z <-> x e. z ) )
95 94 notbid 
 |-  ( u = x -> ( -. u e. z <-> -. x e. z ) )
96 95 spvv 
 |-  ( A. u -. u e. z -> -. x e. z )
97 96 pm2.21d 
 |-  ( A. u -. u e. z -> ( x e. z -> x e. y ) )
98 97 a1i 
 |-  ( -. A. x x = z -> ( A. u -. u e. z -> ( x e. z -> x e. y ) ) )
99 39 93 98 alrimdd 
 |-  ( -. A. x x = z -> ( A. u -. u e. z -> A. x ( x e. z -> x e. y ) ) )
100 88 99 pm2.61i 
 |-  ( A. u -. u e. z -> A. x ( x e. z -> x e. y ) )
101 82 100 syl6 
 |-  ( A. u -. u e. y -> ( z = y -> A. x ( x e. z -> x e. y ) ) )
102 elequ1 
 |-  ( u = z -> ( u e. y <-> z e. y ) )
103 102 notbid 
 |-  ( u = z -> ( -. u e. y <-> -. z e. y ) )
104 103 spvv 
 |-  ( A. u -. u e. y -> -. z e. y )
105 104 pm2.21d 
 |-  ( A. u -. u e. y -> ( z e. y -> A. x ( x e. z -> x e. y ) ) )
106 101 105 jaod 
 |-  ( A. u -. u e. y -> ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
107 106 a1i 
 |-  ( -. A. y y = z -> ( A. u -. u e. y -> ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
108 21 78 107 alrimdd 
 |-  ( -. A. y y = z -> ( A. u -. u e. y -> A. z ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
109 4 108 eximd 
 |-  ( -. A. y y = z -> ( E. y A. u -. u e. y -> E. y A. z ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
110 72 109 mpi 
 |-  ( -. A. y y = z -> E. y A. z ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
111 nfae 
 |-  F/ y A. x x = y
112 nfae 
 |-  F/ z A. x x = y
113 equequ2 
 |-  ( x = y -> ( z = x <-> z = y ) )
114 113 sps 
 |-  ( A. x x = y -> ( z = x <-> z = y ) )
115 114 orbi1d 
 |-  ( A. x x = y -> ( ( z = x \/ z e. y ) <-> ( z = y \/ z e. y ) ) )
116 115 imbi1d 
 |-  ( A. x x = y -> ( ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) <-> ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
117 112 116 albid 
 |-  ( A. x x = y -> ( A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) <-> A. z ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
118 111 117 exbid 
 |-  ( A. x x = y -> ( E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) <-> E. y A. z ( ( z = y \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
119 110 118 imbitrrid 
 |-  ( A. x x = y -> ( -. A. y y = z -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) ) )
120 71 119 pm2.61d 
 |-  ( A. x x = y -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
121 nfae 
 |-  F/ z A. x x = z
122 87 a1d 
 |-  ( A. x x = z -> ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
123 121 122 alrimi 
 |-  ( A. x x = z -> A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
124 123 19.8ad 
 |-  ( A. x x = z -> E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) ) )
125 61 120 124 70 pm2.61iii 
 |-  E. y A. z ( ( z = x \/ z e. y ) -> A. x ( x e. z -> x e. y ) )